-
Notifications
You must be signed in to change notification settings - Fork 41
/
lection06.tex
156 lines (152 loc) · 11.2 KB
/
lection06.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
\section{Лекция 6 \\ Реконструкция типов в просто типизированном \\ $\lambda$-исчислении, комбинаторы}
\subsection{Алгоритм вывода типов}
Пусть есть: $?\:\vdash \:A\: :\: ?$, хотим найти пару $\big \langle \text{контекст}, \text{тип} \big \rangle$\par
\textbf{Алгоритм:}
\begin{enumerate}
\item Рекурсия по структуре формулы\par Построить по формуле $A$ пару $\big \langle E, \tau\big \rangle$, где\par $E-$система уравнений, $\tau-$тип $A$
\item Решение уравнения, получение подстановки $S$ и из решения $E$ и $S\:(\tau)$ получение ответа
\end{enumerate}
Т.е. необходимо свести вывод типа к алгоритму унификации.\par
\begin{oun_paragraph}Рассмотрим 3 случая\end{oun_paragraph}
\textbf{Обозначение } $\rightarrow-$ алгебраический тип
\begin{enumerate}
\item $A\equiv x\implies\:\big \langle \{\}, \alpha_x\big\rangle$, где $\{\}-$пустой контекст
\item $A\equiv P\:Q\implies\big \langle E_P\cup E_Q\cup \{\tau_P=\:\rightarrow\:(\tau_Q\:\alpha_A)\}, \alpha_A\big \rangle$, где $\alpha_A-$новая переменная
\item $A\equiv\lambda x.P\implies\big\langle E_P,\alpha_x\:\rightarrow\:\tau_P\big\rangle$
\end{enumerate}
\begin{oun_paragraph}Алгоритм унификации\end{oun_paragraph}
Рассмотрим $E-$систему уравнений, запишем все уравнения в алгебраическом виде, т.е. \par $\alpha\:\rightarrow\:\beta\:\Leftrightarrow\:\rightarrow\:\alpha\:\beta$, затем применяем алгоритм унификации.
\begin{lemma}
Рассмотрим терм $M$ и пару $\big\langle E_M, \tau_M\big\rangle$, Если $\Gamma\:\vdash M:\rho$, то существует:
\end{lemma}
\begin{enumerate}
\item $S-$решение $E_M$ тогда $\Gamma=\{x : S(\alpha_x)\:|\:x\in FV(M)\}$, $FV-$множество свободных переменных в терме $M$, $\alpha_x-$ переменная, полученная при разборе терма $M$\par
$\rho\:=\:S(\tau_M)$
\item Если $S-$ решение $E_M$, то $\Gamma\:\vdash M:\rho$,
\begin{proof}индукция по структуре терма $M$
\begin{enumerate}
\item Если $M\equiv x$, то так как решение существует, то существует и $S(\alpha_x)$, что: \par$\Gamma,\:x:S(\alpha_x)\:\vdash \:x:S(\alpha_x)$
\item Если $M\equiv \lambda x.\:P$, то по индукции уже известен тип $P$, контекст $\Gamma$ и тип $x$, тогда: $${\Gamma,\:x:\:S(\alpha_x)\:\vdash \:P:\:S(\alpha_P) \over \Gamma\:\vdash \:\lambda x.\:P:S(\alpha_x)\:\rightarrow\:S(\alpha_P)}$$
\item Если $M\equiv P\:Q$, то по индукции: $${ \Gamma\:\vdash \:P:\:S(\alpha_P)\equiv\tau_1\:\rightarrow\:\tau_2 \hspace{4em} \Gamma\:\vdash \:Q:S(\alpha_Q)\equiv\tau_1\over \Gamma\:\vdash \:P\:Q:\tau_2}$$
\end{enumerate}
\end{proof}
\end{enumerate}
$\big \langle\Gamma,\tau\big\rangle\:-\:$основная пара для терма $M$, если
\begin{enumerate}
\item $\Gamma\:\vdash M:\tau$
\item Если $\Gamma'\:\vdash M:\tau'$, то существует $S:\:S(\Gamma)\:\subset\:\Gamma'$
\end{enumerate}
\begin{example}
\end{example}
Рассмотрим терм: $\lambda f\:\lambda x.\:f(f(x))$, построим и пронумеруем его дерево разбора:\par
\begin{tikzpicture}
\node [fill=none, draw=none] (A) at (4,0) {$\lambda f\:\lambda x.\:f(f(x))\enspace{\color{blue} (7)}$};
\node [fill=none, draw=none] (B) at (7.5,-1) {$\lambda x.\:f(f(x))\enspace{\color{blue} (6)}$};
\node [fill=none, draw=none] (C) at (2,-1) {$\lambda f$};
\node [fill=none, draw=none] (D) at (10.5,-2) {$f(f(x))\enspace{\color{blue} (5)}$};
\node [fill=none, draw=none] (E) at (5.5,-2) {$\lambda x$};
\node [fill=none, draw=none] (F) at (13.5,-3) {$f(x)\enspace{\color{blue} (4)}$};
\node [fill=none, draw=none] (G) at (8.5,-3) {$f\enspace{\color{blue} (3)}$};
\node [fill=none, draw=none] (H) at (11.5,-4) {$f\enspace{\color{blue} (2)}$};
\node [fill=none, draw=none] (I) at (16.5,-4) {$x\enspace{\color{blue} (1)}$};
\path [->] (A) edge node[left] {} (B);
\path [->] (A) edge node[left] {} (C);
\path [->] (B) edge node[left] {} (D);
\path [->] (B) edge node[left] {} (E);
\path [->] (D) edge node[left] {} (F);
\path [->] (D) edge node[left] {} (G);
\path [->] (F) edge node[left] {} (H);
\path [->] (F) edge node[left] {} (I);
\end{tikzpicture}\par
\begin{enumerate}
\item $\big\langle E_1, \tau_1\big\rangle=\big \langle \{\},\:\alpha_x \big \rangle$
\item $\big\langle E_2, \tau_2\big\rangle=\big \langle \{\},\:\alpha_f \big \rangle$
\item $\big\langle E_3, \tau_3\big\rangle=\big \langle \{\},\:\alpha_f \big \rangle$
\item $\big\langle E_4, \tau_4\big\rangle=\big \langle \{\alpha_f=\:\rightarrow(\alpha_x\:\alpha_1)\}, \alpha_1 \big \rangle$
\item $\big\langle E_5, \tau_5\big\rangle=\big \langle \begin{Bmatrix}
\alpha_f=\:\rightarrow(\alpha_x\:\alpha_1)\\
\alpha_f=\:\rightarrow(\alpha_1\:\alpha_2)
\end{Bmatrix},\:\alpha_2 \big \rangle$
\item $\big\langle E_6, \tau_6\big\rangle=\big \langle \begin{Bmatrix}\alpha_f=\:\rightarrow(\alpha_x\:\alpha_1)\\ \alpha_f=\:\rightarrow(\alpha_1\:\alpha_2)\end{Bmatrix},\:\alpha_x\rightarrow\alpha_2 \big \rangle$
\item $\big\langle E_7, \tau_7\big\rangle=\big \langle \begin{Bmatrix}\alpha_f=\:\rightarrow(\alpha_x\alpha_1)\\ \alpha_f=\:\rightarrow(\alpha_1\alpha_2)\end{Bmatrix},\:\alpha_f\rightarrow(\alpha_x\rightarrow\alpha_2) \big \rangle$
\end{enumerate}
$E=\begin{Bmatrix}\alpha_f=\:\rightarrow\:(\alpha_x\:\alpha_1)\\ \alpha_f=\:\rightarrow\:(\alpha_1\:\alpha_2)\end{Bmatrix}$, решим полученную систему:\par
\begin{enumerate}
\item Решим систему:\par
\begin{enumerate}
\item \[
\begin{cases}
\alpha_f = \rightarrow(\alpha_x\:\alpha_1)\\
\alpha_f = \rightarrow(\alpha_1\:\alpha_2)\\
\end{cases}\]
\item \[
\begin{cases}
\alpha_f = \rightarrow(\alpha_x\:\alpha_1)\\
\rightarrow(\alpha_1\:\alpha_2) = \rightarrow(\alpha_x\:\alpha_1)\\
\end{cases}\]
\item \[
\begin{cases}
\alpha_f = \rightarrow(\alpha_x\:\alpha_1)\\
\alpha_1 = \alpha_x\\
\alpha_2 = \alpha_1\\
\end{cases}\]
\item \[
\begin{cases}
\alpha_f = \rightarrow(\alpha_x\:\alpha_x)\\
\alpha_1 = \alpha_x\\
\alpha_2 = \alpha_x\\
\end{cases}\]
\end{enumerate}
\item Получим \[S=\begin{cases}
\alpha_f=\rightarrow(\alpha_x\:\alpha_x)&\\
\alpha_1=\alpha_x&\\
\alpha_2=\alpha_x&\\
\end{cases}\]
\item $\Gamma=\{\}$, так как в заданной формуле нет свободных переменных
\item Тип терма $\lambda\:f\lambda\:x.f(f(x))$ является результатом подстановки\par $S(\rightarrow\:\alpha_f\:(\alpha_x\rightarrow\alpha_2))$, получаем $\tau=(\alpha_x\rightarrow\alpha_x)\rightarrow(\alpha_x\rightarrow\alpha_x)$
\end{enumerate}
\subsection{Сильная и слабая нормализации}
\begin{definition}Если существует последовательность редукций, приводящая терм $M$ в нормальную форму, то $M-$слабо нормализуем. (Т.е. при редуцировании терма $M$ мы можем не прийти в н.ф.)\end{definition}
\begin{definition}Если не существует бесконечной последовательности редукций терма $M$, то терм $M-$ сильно нормализуем.\end{definition}
\begin{statement}
\end{statement}
\begin{enumerate}
\item $KI\Omega-$ слабо нормализуема
\begin{example}\end{example}
Перепишем $KI\Omega$ как ${\color{red}(}(\lambda x\:\lambda y.\:x)(\lambda x.\:x){\color{red})}{\color{blue}(}((\lambda x.\:x\:x)(\lambda x.\:x\:x)){\color{blue})}$, очевидно, что этот терм можно средуцировать двумя разными способами:\\
\begin{enumerate}
\item Сначала редуцируем красную скобку
\begin{enumerate}
\item ${\color{red}(}(\lambda x\:\lambda y.\:x)(\lambda x.\:x){\color{red})}{\color{blue}(}((\lambda x.\:x\:x)(\lambda x.\:x\:x)){\color{blue})}$
\item ${\color{red}(}(\lambda y.\:(\lambda x.\:x)){\color{red})}{\color{blue}(}((\lambda x.\:x\:x)(\lambda x.\:x\:x)){\color{blue})}$
\item $(\lambda x.\:x)$
\end{enumerate}
Видно, что в этом случае количество шагов конечно.
\item Редуцируем синюю скобку. Очевидно, что комбинатор $\Omega$ не имеет нормальной формы, тогда понятно, что в этом случае терм $KI\Omega$ никогда не средуцируется в нормальную форму.
\end{enumerate}
\item $\Omega-$ не нормализуема
\item $II-$ сильно нормализуема
\end{enumerate}
\begin{lemma}Сильная нормализация влечет слабую.
\end{lemma}
\subsection{Выразимость комбинаторов}
\begin{statement}Для любого $\lambda$-выражения без свободных переменных существует $\beta$-эквивалентное ему выражение, записываемое только с помощью комбинаторов $S$ и $K$, где\end{statement}
$S\:=\:\lambda x\:\lambda y\:\lambda z.\:(x\:z)\:(y\:z)\: : \:(a\:\rightarrow\:b\:\rightarrow\:c)\:\rightarrow\:(a\:\rightarrow\:b)\:\rightarrow\:a\:\rightarrow\:c$\par
$K=\lambda x\:\lambda y.\:x\: : a\:\rightarrow\:b\:\rightarrow\:a$\par
\begin{statement}Комбинаторы $S$ и $K$ являются аксиомами в ИИВ\end{statement}
\begin{statement}Соотношение комбинаторов с $\lambda$ исчислением:\end{statement}
\begin{enumerate}
\item $T(x)=x$
\item $T(P\:Q)=T(P)\:T(Q)$
\item $T(\lambda\:x.P)=K(T(P)),\enspace x\not\in FV(P)$
\item $T(\lambda\:x.x)=I$
\item $T(\lambda\:x\lambda\:y.P)=T(\lambda\:x.\:T(\lambda\:y.P))$
\item $T(\lambda\:x.P\:Q)=S\:\:T(\lambda\:x.P)\:T(\lambda\:x.Q)$
\end{enumerate}
\begin{statement}Альтернативный базис:\end{statement}
\begin{enumerate}
\item $B=\lambda x\:\lambda y\:\lambda z.\:x\:(y\:z)\: : \:(a\:\rightarrow\:b)\:\rightarrow\:(c\:\rightarrow\:a)\:\rightarrow\:c\:\rightarrow\:b$
\item $C=\lambda x\:\lambda y\:\lambda z.\:((x\:z)\:y)\: : \:(a\:\rightarrow\:b\:\rightarrow\:c)\:\rightarrow\:b\:\rightarrow\:a\:\rightarrow\:c$
\item $K=\lambda x\:\lambda y.\:x : a\:\rightarrow\:b\:\rightarrow\:a$
\item $W=\lambda x\:\lambda y.\:((x\:y)\:y)\: : \: (a\:\rightarrow\:a\:\rightarrow\:b)\:\rightarrow\:a\:\rightarrow\:b$
\end{enumerate}