lection07.tex

\section{Лекция 7}
	\subsection{Импликационный фрагмент ИИП второго порядка}
 	\begin{center}
 		\begin{definition}
 			Назовем \textit{\underline{грамматикой ИИП второго порядка}} конструкцию вида: 
 		\end{definition}
 	\textbf{A} ::=
 	\textbf{p} |
	(\textbf{A} $\rightarrow$ \textbf{A}) |
	($\forall$\textbf{p}.\textbf{A})
 	
 	\end{center}
 
 	В этой системе все остальные связки могут быть выражены через основные 4, представленные выше. Например, $\perp$ представима в следующем виде
 	\begin{center}
 		{\textbf{\textsl\textit{$\forall$p.p}}} \\
 	\end{center}
 	
 	
 	 Также добавим два новых правила вывода для квантора существования и два для квантора всеобщности к уже существующим в ИИВ: \\ \\
 	
	Для квантора всеобщности: \\ 
 	
    \[ \dfrac{\Gamma\vdash\phi}{\Gamma\vdash\forall p.\phi} (p\notin FV(\Gamma)) \qquad
        \dfrac{\Gamma\vdash\forall p.\phi}{\Gamma\vdash\phi[p:=\Theta]} \]
 	
 	 И два для квантора существования: \\
 	
    \[ \dfrac{\Gamma\vdash\phi[p:= \psi]}{\Gamma\vdash\exists p.\phi}\qquad
        \dfrac{\Gamma\vdash\exists p.\phi\quad\Gamma, \phi\vdash\psi}{\Gamma\vdash\psi} (p\notin FV(\Gamma, \psi)) \]
 	
 	
 	\begin{definition}
 		Грамматику ИИП второго порядка с приведенными выше правилами вывода назовем Импликационным фрагментом ИИВ второго порядка\\ 
 	\end{definition}
	{С помощью этих правил вывода можно доказать, что \textbf{${\perp = \forall p.p}$}
		Действительно, воспользовавшись вторым правилом вывода квантора всеобщности для этого выражения, мы можем вывести любое другое выражение.}
 	
 	С помощью правил вывода также можно доказать, что \\
 	$\phi\&\psi\equiv\forall a. ((\phi\rightarrow\psi\rightarrow a)\rightarrow a)$\\
 	$\phi\vee\psi\equiv\forall a. ((\phi\rightarrow a)\rightarrow(\psi\rightarrow a)\rightarrow a)$
 	
 	Докажем например, что
 	\begin{center}
 		 $\dfrac{\Gamma\vdash\perp}{\Gamma\vdash \phi}$
 	\end{center}
 	Воспользуемся вторым правилом вывода для квантора всеобщности
 	\begin{center}
		$\dfrac{\Gamma\vdash\forall\alpha.\alpha}{\Gamma\vdash\alpha[\alpha:=\phi]} $
 	\end{center}
 	
 	\subsection{Теория Моделей}
	Добавим к нашему исчислению модель. Напомню, что модель это функция которая сопоставляет некому терму элемент из множества истинностных значений. В нашем случае мы будем сопоставлять высказываниям элементы из множества $\llbracket\text{\textbf{И,Л}}\rrbracket$ по следующим правилам: \\

\begin{center}
	 	$\llbracket p\rrbracket=p$, т. е. $\llbracket p\rrbracket^{p = x} = x$ \\
\end{center}
 	
 	
 \begin{center}
 		\begin{equation*}
 		\llbracket p\rightarrow Q\rrbracket = 
 		\begin{cases}
 			\text{Л}, \llbracket p\rrbracket = \text{И}, \llbracket Q\rrbracket = \text{Л} \\
 			\text{И}, \text{иначе}
 		\end{cases}
 	\end{equation*}
 \end{center}
 	
 	
 	\begin{equation*}
 		\llbracket\forall p.Q\rrbracket = 
 		\begin{cases}
 			\text{И}, \llbracket Q\rrbracket^{p=\text{л, и}} = \text{И} \\
 			\text{Л}, \text{иначе}
 		\end{cases}
 	\end{equation*}
 	Эта модель корректна, но не полна.
 	
 	\subsection{Система F}
 	
\begin{definition}
	 	Под типом в системе F будем понимать следующее

 	
 	\begin{equation*}
 	\tau =
 	\begin{cases}
 	\alpha,\beta,\gamma ...\quad(\text{атомарные типы}) \\
 	\tau\rightarrow\tau \\
 	\forall\alpha.\tau\qquad(\alpha\text{ - переменная})
 	\end{cases}
 	\end{equation*}
 \end{definition}

 \begin{definition}
 		Введем определение грамматики в системе F:
 	\begin{center}
		$\mathcal{L}$ ::= x | $\left(\lambda x^{\tau}.\mathcal{L}\right)$ | $\left(\mathcal{L}\ \mathcal{L}\right)$ | $\left(\Lambda\alpha.\mathcal{L}\right)$ | $\left(\mathcal{L}\tau\right)$
 	\end{center}
 \end{definition}
 	
	где $\Lambda\alpha.\Lambda$ --- типовая абстракция, явное указание того, что вместо каких-то типов мы можем подставить любые выражения, а $\Lambda\tau$ --- это применение типа. \\
 	
 	
 	Так, пример типовой абстракции это: 
    \begin{minted}{cpp}
template<typename T>
class W {
    T x;
}
    \end{minted}
 	
	Типовая аппликация --- это объявление переменной класса с каким-то типом
 	
    \begin{minted}{cpp}
W<int> w_test;
    \end{minted}
 	
 	\begin{theorem}
 		Изоморфизм Карри - Ховарда:
    \begin{center}
 		$\Gamma\vdash_F M:\tau\Leftrightarrow |\Gamma|\vdash_{\forall, \rightarrow}\tau$ 
    \end{center}
 	
 	\end{theorem}
 	
 	
 	
 	В системе F определены следующие правила вывода: \\ \\
  	\noindent
 	{$\dfrac{}{\Gamma,x:\tau\vdash x:\tau}\qquad\qquad$} 
 	{$\dfrac{\Gamma\vdash M:\sigma\rightarrow\tau\qquad\Gamma\vdash N:\sigma}{\Gamma\vdash M N:\tau}$}\\  \\ \\
 	{$\dfrac{\Gamma,x:\tau\vdash M:\sigma}{\Gamma\vdash\lambda x^{\tau}.M:\tau\rightarrow\sigma}\quad(x\notin FV(\Gamma))$}\\ \\ \\
 	{$\dfrac{\Gamma\vdash M:\sigma}{\Gamma\vdash\Lambda\alpha.M:\forall\alpha.\sigma}\quad(\alpha\notin FV(\Gamma))\qquad$}
 	 $\dfrac{\Gamma\vdash M:\forall\alpha.\sigma}{\Gamma\vdash M\tau:\sigma[\alpha:=\tau]}$
 	\\
 	
 	$\emph{Приведем пример}$. Покажем как выглядит в системе F левая проекция.
 	В просто типизированном $\lambda$ - исчислении $\pi_1$ имеет тип $\alpha\&\beta\rightarrow\alpha$. В системе F явно указывается, что элементы пары могут быть любыми и пишется соответственно $\forall\alpha.\forall\beta.\alpha\&\beta\rightarrow\alpha$. Само выражение для проекции также изменится и будет иметь вид  $\pi_1=\Lambda\alpha.\Lambda\beta.\lambda p^{\alpha\&\beta}.p\rm{T}$
 	
 	Давайте определим еще несколько понятий из простого $\lambda$-исчисления. \\
    \emph{Начнем с $\beta$-редукции:}
    \begin{enumerate}
        \item Типовая $\beta$-редукция: $(\Lambda\alpha.M^{\sigma})\tau\rightarrow_\beta M[\alpha:= \tau]:\sigma[\alpha:= \tau]$
        \item Классическая $\beta$-редукция: $(\lambda x^{\sigma}.M)^{\sigma\rightarrow\tau}X\rightarrow_\beta M[x:=X]:\tau$ 
    \end{enumerate}
 	\emph{Выразим еще несколько функций} \\
 	
    \begin{enumerate}
        \item Не бывает М:$\perp$
        \item Рассмотрим пару <P, Q> ::= $\Lambda\alpha.\lambda z^{\tau\rightarrow\sigma\rightarrow\alpha}.z P Q$ \\
            Проекторы мы рассмотрели ранее.
        \item $in_L(M^{\tau}) ::= \Lambda\alpha.\lambda u^{\tau\rightarrow\alpha}.\lambda\omega^{\sigma\rightarrow\alpha}.u M$\\
            $ in_R(M^{\sigma}) ::= \Lambda\alpha.\lambda u^{\tau\rightarrow\alpha}.\lambda\omega^{\sigma\rightarrow\alpha}.u M$\\
    \end{enumerate}
 	

 	
    \begin{enumerate}
        \item Теорема Чёрча-Россера и прочие теоремы, доказуемые в просто-типизированном лямбда-исчислении, доказуемы и в системе F
 	    \item $\lambda_{(\forall, \rightarrow)}$ Система F сильно нормализуема
 	    \item Y комбинатор не типизируем
	    \item Исчисление неразрешимое, но не противоречивое
    \end{enumerate}