Skip to content
Permalink
Browse files

Some change

  • Loading branch information
shd
shd committed Mar 24, 2015
1 parent dbab53f commit 1ef6f2b6d0c9af1e883fdf3cca9e18072af396ae
Showing with 701 additions and 215 deletions.
  1. +4 −0 .gitignore
  2. +4 −2 conspect.tex
  3. +16 −14 hw.tex
  4. +77 −0 lection2.tex
  5. +178 −37 lection3.tex
  6. +121 −0 lection4.tex
  7. +93 −0 lection4a.tex
  8. +53 −0 lection5a.tex
  9. +113 −107 lection6.tex
  10. +24 −55 lection7.tex
  11. +18 −0 lection8.tex
@@ -0,0 +1,4 @@
*.aux
*.dvi
*.log
*~
@@ -27,7 +27,8 @@
\newcommand{\+}{\lambda}
\newcommand{\bredmath}{\ \longrightarrow_\beta\ }
\newcommand{\bred}{$\bredmath$}
\newcommand{\mbred}{$\ \longrightarrow\!\!\!\!\rightarrow_\beta\ $}
\newcommand{\mbredmath}{\ \longrightarrow\!\!\!\!\rightarrow_\beta\ }
\newcommand{\mbred}{$\mbredmath$}
\newcommand{\lid}[1]{\textit{#1}}
\newcommand{\concat}{\hat{\ \ }}

@@ -39,8 +40,9 @@
{\begin{list}{}{\setlength{\leftmargin}{0.3\textwidth}}\item[]}%
{\end{list}}

%\include{lection1}
\include{lection2}
\include{lection3}
\include{lection4}
\include{lection5}
\include{lection6}
\include{lection7}
30 hw.tex
@@ -130,14 +130,16 @@

\begin{bnf}\begin{eqnarray*}
<\nt{Выражение}> & ::= & \chr{let} <\nt{Переменная}> \chr{=} <\nt{Выражение}> \chr{in} <\nt{Выражение}>\\
& | & <\nt{Абстракция}>\\
<\nt{Абстракция}> & ::= & [<\nt{Применение}>] \chr{\textbackslash{}} <\nt{Переменная}> \chr{.} <\nt{Абстракция}> \\
& | & <\nt{Применение}> \\
<\nt{Применение}> & ::= & <\nt{Применение}> <\nt{Терм}> | <\nt{Терм}> \\
<\nt{Терм}> & ::= & \chr{(} <\nt{Абстракция}> \chr{)} | <\nt{Значение}> \\
<\nt{Значение}> & ::= & (\chr{a}\dots\chr{z}) \rep{\chr{0}\dots\chr{9}}{*} \rep{\chr{\'}}{*}\\
<\nt{Терм}> & ::= & \chr{(} <\nt{Выражение}> \chr{)} \\
& | & <\nt{Переменная}>\\
& | & \chr{F}|\chr{T}|\chr{If}|\chr{Y}|\chr{Plus}|\chr{Minus}|\chr{Eq}|\rep{\chr{0}\dots\chr{9}}{+}\\
& | & \chr{<}<\nt{Значение}>\chr{,}<\nt{Значение}>\chr{>} | \chr{PrL} | \chr{PrR}\\
& | & \chr{InL} | \chr{InR} | \chr{Case}
& | & \chr{<}<\nt{Выражение}>\chr{,}<\nt{Выражение}>\chr{>} | \chr{PrL} | \chr{PrR}\\
& | & \chr{InL} | \chr{InR} | \chr{Case}\\
<\nt{Переменная}> & ::= & (\chr{a}\dots\chr{z}) \rep{\chr{0}\dots\chr{9}}{*} \rep{\chr{\'}}{*}
\end{eqnarray*}\end{bnf}%
Аналогично простым лямбда-выражениям,
если подряд указаны какие-либо идентификаторы или ключевые слова \chr{let} и \chr{in},
@@ -158,9 +160,9 @@
\chr{Eq x y} & если $x$, $y$ --- не числа, то ошибка; если $x=y$, то \chr{T}, иначе \chr{F}\\
\chr{Y f} & \chr{f (Y f)}\\
\chr{PrL <a,b>} & \chr{a}\\
\chr{PrL <a,b>} & \chr{b}\\
\chr{Case (PrL x) l r} & \chr{l x}\\
\chr{Case (PrR y) l r} & \chr{r y}
\chr{PrR <a,b>} & \chr{b}\\
\chr{Case (InL x) l r} & \chr{l x}\\
\chr{Case (InR y) l r} & \chr{r y}
\end{tabular}%

Частичное применение переменных особого вида допускается (в этом случае имеет
@@ -200,18 +202,18 @@
Имя & Тип\\
\hline
T,F & $Bool$\\
If & $Bool \rightarrow a \rightarrow a \rightarrow a $\\
If & $\forall a (Bool \rightarrow a \rightarrow a \rightarrow a) $\\
$0,1,\dots,2^{63}-1$ & $Int$\\
Plus & $Int \rightarrow Int \rightarrow Int$\\
Minus & $Int \rightarrow Int \rightarrow Int$\\
Eq & $Int \rightarrow Int \rightarrow Bool$\\
$< x^a, y^b >$ & $a \& b$\\
PrL & $a\&b \rightarrow a$\\
PrR & $a\&b \rightarrow b$\\
InL & $a \rightarrow a | b$\\
InR & $a \rightarrow a | b$\\
Case & $a | b \rightarrow (a\rightarrow c) \rightarrow (b\rightarrow c) \rightarrow c$\\
Y & $(a \rightarrow a) \rightarrow a$
PrL & $\forall a \forall b (a\&b \rightarrow a)$\\
PrR & $\forall a \forall b (a\&b \rightarrow b)$\\
InL & $\forall a \forall b (a \rightarrow a | b)$\\
InR & $\forall b \forall b (b \rightarrow a | b)$\\
Case & $\forall a \forall b \forall c (a | b \rightarrow (a\rightarrow c) \rightarrow (b\rightarrow c) \rightarrow c)$\\
Y & $\forall a ((a \rightarrow a) \rightarrow a)$
\end{tabular}%

Убедитесь, что решения для примеров из предыдущей задачи правильно типизируются.
@@ -0,0 +1,77 @@
\section{Парадокс Карри}

Лямбда-исчисление было предложено Черчем в начале 1930х годов
для формализации математики. Особенность лямбда-исчисления,
отличающего его от, допустим, обычного исчисления предикатов ---
формализация понятия применения функций. В лямбда-исчислении легко
выражаются сложные понятия --- например, натуральные числа,
причем это достигается без введения дополнительного набора аксиом
как в формальной арифметике.

Однако, довольно быстро в нем нашлись неустранимые парадоксы.
Далее будет изложен один из парадоксов, это не оригинальный парадокс
1932 года --- поскольку современное лямбда-исчисление появилось в 1940
году как результат упрощения Черчем исходной теории. Но пример
дает представление о проблеме.

Построим исчисление высказываний на основе языка лямбда-выражений,
добавив в паре к аппликации импликацию.
В таком языке функция $\lambda f.\lambda x.f x \rightarrow f x$
являлась бы тавталогией. Естественно, в этом исчислении будут аксиомы
и правила вывода, как и в обычном исчислении предикатов --- среди них
будут и обычные логические аксиомы, и аксиомы про лямбда-преобразования,
и подобным выражениям будет дан четкий формальный смысл.

Мы будем считать, что если $A=_\beta B$, то $\vdash A\rightarrow B$ и
$\vdash B\rightarrow A$.
Удивительно было бы ожидать иного --- ведь результат редукции $A$ и $B$
одинаков (либо обе редукции не заканчиваются).
В программировании бывает, что мы не можем заменить, например,
вызов функции на его результат --- например, \texttt{printf("Hello, world")} нельзя
заменить на $1$, хоть численно их результат равен.
В математике же считается, что разницы между разной записью значений нет.
Иначе получится, что например уравнение $ x^2 = 4 $ выполнено при $x = 2 \cdot \sin \pi$,
но не выполнено при $x = \log_2 4$.

Также мы ожидаем доказуемость
$$\alpha\rightarrow\alpha\rightarrow\beta\vdash\alpha\rightarrow\beta$$ и
$$\alpha\rightarrow\alpha$$ (было бы обидно, если такое нельзя было бы доказать).

%Исчисление получается очень мощным, в частности, в нем мы могли бы выразить
%правило $\alpha\rightarrow\alpha$ как одно выражение $\lambda t.t \rightarrow t$, без
%использования схем аксиом.

В таком исчислении мы могли бы ввести аксиоматику Пеано простыми
определениями (см. ):

И, не вводя никаких дополнительных аксиом, доказать, скажем,
такие утверждения:

Однако, так построенное исчисление черезчур мощно, о чем свидетельствует
следующее рассуждение.

Рассмотрим выражение $F_\alpha \equiv \lambda x. x x \rightarrow \alpha$
и выражение $\Phi_\alpha \equiv F_\alpha F_\alpha$.
Нетрудно видеть, что $\Phi_\alpha =_\beta \Phi_\alpha\rightarrow\alpha$.
Тогда:

\begin{tabular}{ll}
$\vdash\Phi_\alpha\rightarrow\Phi_\alpha$ & Доказуемое утверждение\\
$\vdash\Phi_\alpha\rightarrow\Phi_\alpha\rightarrow\alpha$ & бета-эквивалентность\\
$\vdash(\Phi_\alpha\rightarrow\Phi_\alpha\rightarrow\alpha)\rightarrow(\Phi_\alpha\rightarrow\alpha)$ & Доказуемое утверждение\\
$\vdash\Phi_\alpha\rightarrow\alpha$ & M.P.\\
$\vdash\Phi_\alpha$ & бета-эквивалентность\\
$\vdash\alpha$ & M.P.
\end{tabular}

Таким образом мы показали, что любое утверждение может быть выведено в данной
системе, т.е. система противоречива. Данное противоречие является следствием выразимости
в данной системе парадокса Карри. Парадокс можно продемонстрировать фразой
<<если данное высказывание истинно, то луна сделана из зеленого сыра>> или, чуть более формально,
выражением $\Phi_\alpha = \Phi_\alpha\rightarrow\alpha$ (если выражение истинно,
то из него следует все что угодно).

Данная ситуация хорошо нам знакома и показывает, что механическое перенесение казалось бы
естественных правил в формальные условия может привести к проблемам.

%Подробнее с историей лямбда-исчисления и парадокса Карри можно познакомиться, например, в .

0 comments on commit 1ef6f2b

Please sign in to comment.
You can’t perform that action at this time.