forked from shd/tt2018-conspect
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lection06.tex
152 lines (147 loc) · 10.7 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
\section{Лекция 6 \\ Реконструкция типов в просто типизированном лямбда-исчислении, комбинаторы}
\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_A\big\rangle$, где $\{\}-$пустой конекст, $\alpha_A-$новая переменная нигде не встречавшаяся до этого в формуле
\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,\rho\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 $E_1=\big \langle \{\},\:\alpha_x \big \rangle$
\item $E_2=\big \langle \{\},\:\alpha_f \big \rangle$
\item $E_3=\big \langle \{\},\:\alpha_f \big \rangle$
\item $E_4=\big \langle \{\alpha_f=\:\rightarrow(\alpha_x\:\alpha_1)\}, \alpha_1 \big \rangle$
\item $E_5=\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 $E_6=\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 $E_7=\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}
\rightarrow(\alpha_1\:\alpha_2)=\rightarrow(\alpha_x\:\alpha_1)
\end{cases}\]
\item \[
\begin{cases}
\alpha_1=\alpha_x&\\
\alpha_2=\alpha_1
\end{cases}\]
\item \[
\begin{cases}
\alpha_1=\alpha_x&\\
\alpha_2=\alpha_x
\end{cases}\]
\end{enumerate}
\item Получим \[S=\begin{cases}
\alpha_f=\rightarrow(\alpha_x\:\alpha_1)&\\
\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$ выражение можно записать с помощью комбинаторов $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 $W=\lambda x\:\lambda y.\:((x\:y)\:y)\: : \: (a\:\rightarrow\:a\:\rightarrow\:b)\:\rightarrow\:a\:\rightarrow\:b$
\end{enumerate}