Простые примеры Curry–Howard correspondence

[Dims]

Помогите плиз разобраться.

Допустим, как доказать, что

$((A \implies B) \wedge A) \implies B$

и какой программе это соответствует?

И наоборот, например, программа вычисления длины окружности по формуле

$l = 2 \pi r$

соответствует какому доказательству?

[Xaositect]

Dims в сообщении #417693 писал(а):

и какой программе это соответствует?

Давайте разбираться.
$((A\to B)\wedge A)\to B$ - это импликация.
Импликация соответствует функциональному типу, доказательство - это функция, которая по доказательству $(A\to B)\wedge A$ получает доказательство $B$.
$(A\to B)\wedge A$. Конъюнкция соответствует типу кортежей: доказательство $(A\to B)\wedge A$ - это пара доказательств для $A\to B$ и $A$ соотвестсвенно, т.е. элемент типа $(A\to B)\times A$.
Т.о. нам дано доказательство $(A\to B)\wedge A$ - пара $(f, p)$, где $f$ - элемент $A\to B$, т.е. функция, преобразующая $A$ в $B$, и $p$ - элемент $A$, и надо построить по этой паре какой-то элемент типа $B$. Это будет $f\ p$, а соотвествующий элемент функционального типа $((A\to B)\times A)\to B$, т.е. док-во предложения $((A\to B)\wedge A)\to B$ - $\lambda (f, p). (f\ p)$, или, более строго, $\lambda t^{(A\to B)\times A} . ((\mathrm{proj}_1\ t) (\mathrm{proj}_2\ t))$, где $\mathrm{proj}_i$ - это проекции $((A\to B)\times A) \to (A\to B)$ и $((A\to B)\times A) \to A$

-- Сб фев 26, 2011 20:29:29 --

Dims в сообщении #417693 писал(а):

соответствует какому доказательству?

Вопрос мне кажется немного некорректным, но если подходить формально, то $Double\to Double$. Если точнее, то это следствие из постулатов $2\colon Double$, $\pi\colon Double$ и $\cdot\colon Double\times Double\to Double$.

-- Сб фев 26, 2011 20:37:53 --

Да, соответственно по элементу $\lambda t^{(A\to B)\times A}. ((\mathrm{proj}_1\ t)(\mathrm{proj}_2\ t))$ типа $((A\to B)\times A)\to B$ можно построить формальное доказательство утверждения $((A\to B)\wedge A)\to B$ с помощью теоремы о дедукции:
1.$(A\to B)\wedge A$ - гипотеза ($t\colon (A\to B)\times A$)
2.$((A\to B)\wedge A)\to (A\to B)$ - аксиома ($\mathrm{proj}_1\colon ((A\to B)\times A)\to (A\to B)$)
3.$(A\to B)$ - следствие из 1 и 2 ($\mathrm{proj}_1\ t\colon A\to B$)
4.$((A\to B)\wedge A)\to A$ - аксиома ($\mathrm{proj}_2\colon ((A\to B)\times A)\to A$)
5.$A$ - следствие из 1 и 4 ($\mathrm{proj}_2\ t\colon A$)
6.$B$ - следствие из 3 и 5 ($(\mathrm{proj}_1\ t)(\mathrm{proj}_2\ t)\colon B$)
---
7.$((A\to B)\wedge A)\to B$ по теореме о дедукции из вывода [1-6] ($\lambda t^{(A\to B)\times A}. ((\mathrm{proj}_1\ t)(\mathrm{proj}_2\ t)) \colon ((A\to B)\times A)\to B$)

[Dims]

Что-то я не врубаюсь. Так какая же программа, получается, соответствует доказательству первой формулы?

И что, получается, можно рассматривать и такие объекты, как "доказательство A->B", которые являются недоказуемыми?

Правильно ли я понимаю, что A->B соответствует программе

string F(string x) {
   if(x=="A") return "B";
   else return null;
}

так?

-- Сб фев 26, 2011 21:19:52 --

Xaositect в сообщении #417698 писал(а):

Если точнее, то это следствие из постулатов $2\colon Double$, $\pi\colon Double$ и $\cdot\colon Double\times Double\to Double$.

Не понял. Вы говорите, что программа, вычисляющая длину окружности, соответствует доказательству того, что произведение двух вещественных вещественно? Но тогда получается, что любая программа, производящая вычисления с вещественными числами, соответствует одному и тому же доказательству?

Значит, получается, соответствие не взаимно-однозначное?

Иными словами, доказательство, соответствующее какой-либо программе, есть просто доказательство того, что тип её результата определённым образом соответствует типам её аргументов? Но это разве не совсем другое? Не правильней ли тогда было говорить, что доказательство соответствует не программе, а алгоритму вывода типа её возвращаемого значения?

[Xaositect]

Dims в сообщении #417722 писал(а):

так?

Нет.
В изоморфизме Карри-Говарда предложениям соответствуют типы данных.
Напр., предложению $A\to B$ соответствует тип всех функций из $A$ в $B$, а доказательством будет любой элемент(по-английски обычно говорят inhabitant) этого типа.
Т.е. доказательством $A\to B$ будет любая функция, если говорить в терминах C, с сигнатурой $\mathtt{B\ f(A\ x)}$.
А самому утверждению соответствует тип $\mathtt{B\ (*)\ (A)}$
А нашему доказательству $((A\to B)\wedge A)\to B$ будет соответствовать такая функция $\mathtt{proof}$:

typedef struct{
  A (*pAimpB) (B x);
  A pA
} AimpBandA;  //тип (A->B)xA

B proof(AimpBandA t)
{
  return t.pAimpB(t.pA);
}

Это если я правильно помню работу с указателями на функции в C

-- Сб фев 26, 2011 21:29:26 --

Dims в сообщении #417722 писал(а):

Иными словами, доказательство, соответствующее какой-либо программе, есть просто доказательство того, что тип её результата определённым образом соответствует типам её аргументов?

Доказательство, соответствующее программе - это доказательство того, что ее тип непуст.

[Dims]

Это абсолютно точно, никаких сомнений? Просто то, что Вы говорите, кажется мне достаточно простым, а то, что мне казалось стоит за фразой "соответствие между программами и доказательствами" казалось совершенно мистическим, поэтому я весьма удивлён.

Иными словами, абсолютно точно, что соответствие не взаимно-однозначное? То есть, множеству программ, делающих совершенно разные вещи, может соответствовать одно доказательство?

А почему A->B соответствует какое-то "доказательство"? Ведь это не тождество? Его же нельзя доказать! Можно доказать $\exists(A,B): A \implies B$, но это же другое выражение.

[Xaositect]

Dims в сообщении #417741 писал(а):

Это абсолютно точно, никаких сомнений? Просто то, что Вы говорите, кажется мне достаточно простым, а то, что мне казалось стоит за фразой "соответствие между программами и доказательствами" казалось совершенно мистическим, поэтому я весьма удивлён.

Ну, это достаточно просто, но если копнуть поглубже, то вылезают разные интересные вещи. Скажем, dependent types. Пруверы, опять же, можно пытаться делать. Формальное доказательство корректности функции можно писать в виде другой функции и т.п.

Dims в сообщении #417741 писал(а):

Иными словами, абсолютно точно, что соответствие не взаимно-однозначное? То есть, множеству программ, делающих совершенно разные вещи, может соответствовать одно доказательство?

Почему же. Разные функции - это разные доказательства того, что их тип непуст. Вот, скажем, тождественная функция Double->Double - это доказательство одно, не зависящее ни от чего, а функция $x\mapsto x^2$ доказывает Double->Double исходя из того, что нам дано умножение, т.е. постулат $\cdot\colon Double\wedge Double \to Double$. Вообще, о конкретных типах в этой области редко говорят, естественнее говорить о полиморфных. Соответственно, функции будут в этом случае затрагивать только структуры данных, а таких вот произвольных постулатов как $\cdot$ не будет. Кстати, таким вот сборникам постулатов соответствуют интерфейсы и type classes.

Dims в сообщении #417741 писал(а):

А почему A->B соответствует какое-то "доказательство"?

Совершенно верно, поэтому полиморфную функцию из произвольного типа в произвольный можно написать только с помощью грязных хаков. Она не имеет математического смысла.
Но если бы доказательство было - то оно соответствовало некоторой полиморфной функции $A\to B$.