2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

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

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

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему
 
 Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 20:12 
Заслуженный участник
Аватара пользователя


16/03/06
406
Moscow
Помогите плиз разобраться.

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

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

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

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

$l = 2 \pi r$

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

 Профиль  
                  
 
 Re: Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 20:27 
Заслуженный участник
Аватара пользователя


06/10/08
6422
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$)

 Профиль  
                  
 
 Re: Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 21:13 
Заслуженный участник
Аватара пользователя


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

И что, получается, можно рассматривать и такие объекты, как "доказательство 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$.

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

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

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

 Профиль  
                  
 
 Re: Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 21:26 
Заслуженный участник
Аватара пользователя


06/10/08
6422
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 писал(а):
Иными словами, доказательство, соответствующее какой-либо программе, есть просто доказательство того, что тип её результата определённым образом соответствует типам её аргументов?
Доказательство, соответствующее программе - это доказательство того, что ее тип непуст.

 Профиль  
                  
 
 Re: Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 21:48 
Заслуженный участник
Аватара пользователя


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

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

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

 Профиль  
                  
 
 Re: Простые примеры Curry–Howard correspondence
Сообщение26.02.2011, 22:17 
Заслуженный участник
Аватара пользователя


06/10/08
6422
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$.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 6 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group