lectureAll.tex

\documentclass[a4paper,10pt]{book}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{tikzcd}

\usepackage{amsthm}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
%\newcommand{\llbracket}{ \llbracket }
\newcommand{\sem}[2]{ \llbracket#1\rrbracket_{#2} }
%\AxiomC{$M=M'$}  
\newcommand{\AxioM}[1]{ \AxiomC{$#1$} }
\newcommand{\rarr}{ \rightarrow }
%\usepackage{fontspec}
%\setmainfont[Ligatures={TeX,Common}]{Linux Libertine O}
\usepackage[a4paper, total={6in, 8in}]{geometry}
\geometry{margin=10mm}

\renewcommand{\tt}{ tt }
\newcommand{\ff}{ ff }

\begin{document}

Dana Scott:  A type-theoretic alternative to ISWIM, CUCH and OWHY (1969, published my TCS in 1993).

\begin{itemize}
\item ICWM by Lundin
\item CUCH is shorten of Curry+Church.
\item OWHY (Oh, what have you)
\end{itemize}

Semantics can be 
\begin{itemize}
\item opertaional (how we evaluate it, abstract machine)
\item logical (describe properties of an object.
\item denotational (words denote some reality; sets which also have formal language)
\item games (actions and reactions from the environment)
\end{itemize}

denotational semantics is often translation from programming languge to set theory. For programmers 
langauges are ``easy`` but set theory is ``hard``.\footnote{
Long very weird history about inventing ``a new math`` by americans to compete with USSR.
And this new math started from teaching sets in schoold as basis of mathematics}

\chapter{Simply typed $\lambda$-calculus}
\paragraph{}

Grammar for types

$\sigma ::= i \mid \sigma \rarr \sigma$
$ \sigma \in \Pi $
Type $ i $ is called initial type.

We define semantics for all the types, having (arbitrary) set $ A_i $ corresponding to initial type.

For set theoretic model, other types are inhabitated as follows: $ A_{\sigma \rightarrow \tau} = A_{\tau}^{A_\sigma}$ that is, set of all total functions from $ A_{\sigma} $ to $ A_{\tau} $


We denote semantic function as $\sem{\cdot}{}$ both for type and calculus terms.

Example of semantics for types: $\sem{i}{} = A_i $

\paragraph{}
Grammar for terms: 
\begin{itemize}
 \item terms $M ::= x \mid MM \mid \lambda x . M$
\end{itemize}

\section{Typing rules}
\paragraph{}
Here we inductively define syntactical mapping between from calculus terms to type terms.

We will write $x^\sigma$ which means that variable has type $\sigma$ (explicit typing in Church-style\footnote{In Church style, we have explicit types for variables,  Curry-style variable has no types}).

% Тут полный пиздец с правилами
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$x^\sigma : \sigma $}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M : \sigma \rarr \tau$} 
\AxiomC{$N: \sigma$} 
\BinaryInfC{$MN : \tau$}
\end{prooftree}

\begin{prooftree}\AxiomC{$M: \tau$}
\AxiomC{}
\BinaryInfC{$(\lambda x^\sigma . M) : \sigma \rarr \tau$}
\end{prooftree}

We will use function $ type $ to get type of term, e.g. $ type(x^i) = i $

We assume, that for every $\sigma$ there 
are infinity many variables of that type.

\section{Abstract \& concrete syntax}

\paragraph{}
In semantics we usually think about abstract syntax. which means a lot of conventions.
E. g. , $\lambda x . x y$ can be lambda from $x$ to $x y$ or identity function applied to $y$.
We need derivation trees to be sure.

% Тут картинка которую я пока не умею рисовать в техе. Отлично, можно отдохнуть.
Another approach instead of derivation is DeBruijn indexes.

\section{Semantics of $\lambda$-calculus}
\paragraph{}

We will inductively define meaning of terms, that is, mapping between terms and certain values.

\paragraph{}

To understand, which value correspond to which variable, we need environment $ \rho $, that is, partial mapping between variables and their values.

$\rho : Var \rightarrow \bigcup_{\sigma \in \Pi} A_\sigma$

\paragraph{}
We will need to introduce bindings to the variables in $ \rho $, that is, extend the environment. For this purpose we will use notation below:

$\rho[x \mapsto a](x) = a$
$\rho[x \mapsto a](y) = \rho(y) $ if $x \neq y$

Semantics of term will be a function from environment $ \rho $ to domain, corresponding the type of term.

The property below is a proposition and actually it should be proven(after semantics is given).

$\sem{M}{\rho} \in A_\sigma$ if $ type(M) = \sigma $

\paragraph{}

Semantics:

$\sem{x^\sigma}{\rho} = \rho(x)$

$\sem{ MN }{\rho} = (\sem{ M }{\rho}) (\sem{N}{\rho})$

$\sem{\lambda x^\sigma . M}{\rho} = (a \mapsto \sem{M}{\rho[x \mapsto a]}) = \lambda a . \sem{M}{\rho[x \mapsto a]}$


% do we need it?
Proposition. If M is well-typed of type $\sigma$ then $\llbracket M\rrbracket_\rho \in
A_\sigma$ where $\rho$ is a var. environment

\subsection{Lemma}
% тут лемма
%TODO: переписать с тетради


\section{Two views}
\begin{itemize}
 \item Sets and functions as a semantics of $\lambda$-calculus.
 \item $\lambda$-calculus is a language to denote sets and functions.
\end{itemize}

Expressivity: how many functions can be defined?

We started from finite sets and built a finite theory from finite types. And let's say we are given a function from finite set to finite set (we can describe it as finite set of pairs). Is this functions $\lambda$-describable.

Let's look: we have a type $i \rightarrow i$. Can we describe function 
$\{T \rightarrow T, F \rightarrow F\}$? Yes, identity for booleans. What about
$\{T \rightarrow T, F \rightarrow T\}$? No.

It's proven that the task is indecidable.(what? which task is undecidable? sounds like bullshit)

\section{Equations}
\paragraph{Axioms of equality as equivalence relation}

\begin{prooftree}
 \AxiomC{}
 \AxiomC{}
 \BinaryInfC{$M=M$}
 %\DisplayProof
\end{prooftree}

\begin{prooftree}
 \AxiomC{$M=N$}
 \AxiomC{$M=P$}
 \BinaryInfC{$M=P$}
 %\DisplayProof
\end{prooftree}

\begin{prooftree}
 \AxiomC{N=M}
 \UnaryInfC{M=N}
\end{prooftree}

\paragraph{Congruence rules}

\begin{prooftree}
 \AxiomC{$M=M'$}
 \AxiomC{$N=N'$}
 \BinaryInfC{$MN=M'N'$}
\end{prooftree}

\begin{prooftree}
 \AxioM{M=M'}
 \UnaryInfC{$\lambda x . M = \lambda x . M'$}
\end{prooftree}

\paragraph{$\beta$-reduction.}

\begin{prooftree}
 \AxioM{}
 \UnaryInfC{$(\lambda x . M)N = M[N/x]$}
\end{prooftree}

\paragraph{$\eta$-expansion}

\begin{prooftree}
 \AxiomC{$x \notin FV(M)$}
 \AxiomC{$M: \sigma \rightarrow \tau$}
 \BinaryInfC{$M = \lambda x^\sigma . M x $}
\end{prooftree}

\paragraph{$\alpha$-conversion}

Actually this one can be inferred from $\beta$ and $\eta$ but is useful

\begin{prooftree}
 \AxiomC{$y \notin FV(M)$}
 \UnaryInfC{$\lambda x . M = \lambda y . M[y/x]$}
\end{prooftree}

We want to know whether the rules are enough to define precisely and syntactically equality for the calculus of functions, therefore we need to answer two questions.

Are these rules correct?

Are these rules complete? (Yes, proved by Friedman).

\paragraph{}
Want: if $M=N$ can be defined then $\sem{M}{\rho} = \llbracket N \rrbracket_\rho$ for any $A_i$  and any $\rho$

After that equivalence and congruence rules are become trivial.

Let's prove that other axioms are OK, (not really weird, sanely chosen ot something like tath).



% $\llbracket (\lambda x .M)N\rrbracket _\rho$ =
% $\llbracket (\lambda x .M)\rrbracket_\rho (\llbracket N\rrbracket_\rho)$ =
% $(a \mapsto \llbracket M\rrbracket\rho[x->a]) (\llbracket N\rrbracket_\rho)$ =
% $\llbracket M \rrbracket _\rho [x -> \llbracket N\rrbracket_\rho]$ 


(Capture avoiding) Substituition Lemma.
$\llbracket M[N/x\rrbracket_\rho = \llbracket M\rrbracket_{\rho
[x \mapsto \llbracket N\rrbracket_\rho]}$

% тут снова картинка чтобы показать композиционность

%байка про то, как в лиспе неправильно сделано подстановки, а Схема всё поправила.
% when you write function it may contain free variable. When we use it later on, LISP
% looks for it in the environment where we use this function
\begin{enumerate}
\item $x[N/x] := N$
\item $y[N/x] := y, y \neq x$
\item $(PM)[N/x] := (P[N/x]) (M[N/x])$
\item $(\lambda x . M)[N/x] := (\lambda x . M)$
\item $(\lambda y . M)[N/x] := (\lambda y . M)[N/x]$ when $y \not\in FV(N)$
\item $(\lambda y . M)[N/x] := \lambda z . (M[z/y])[N/x]$ when $y \in FV(N), z \not\in FV(N) \cup FV(M) \cup \{x\}$
\end{enumerate}

Proofs
\begin{enumerate}
 \item obvious :)
 \item obvious :)
 \item obvious :)
 \item 
 \item The 5th case:

when $y \not\in FV(N)$

$(\lambda y . M)[N/x] = (a \mapsto \llbracket  M[N/x] \rrbracket_{\rho[y \mapsto a]})$

using lemma hypothesis

$ = (a \mapsto \llbracket M\rrbracket_{\rho[y \mapsto a, x \mapsto \llbracket [N/x] \rrbracket_{\rho[z \mapsto a] }]}$


\item 
Now we will prove for the most difficult case (6th) ($\alpha$-equivalence) and others will be exercises.

$\llbracket \lambda z . M[z/y][N/x]\rrbracket_\rho = (a \mapsto 
 \llbracket  M[z/y][N/x] \rrbracket_{\rho[z \mapsto a]})$

using lemma hypothesis
 
$ = (a \mapsto \llbracket M[z/y]\rrbracket_{\rho[z \mapsto a, x \mapsto \llbracket N \rrbracket_{\rho[z \mapsto a] }]})$

symplify

$(a \mapsto \llbracket M[z/y]\rrbracket_{\rho[z \mapsto a, x \mapsto \llbracket N \rrbracket_\rho ]})$

by hypothesis

$(a \mapsto \llbracket M\rrbracket_{\rho[z \mapsto a, x \mapsto \llbracket N \rrbracket_\rho,y \mapsto\llbracket z\rrbracket_{\rho[z \mapsto a, x \mapsto \llbracket N\rrbracket]_\rho ]}})$

symplify

$(a \mapsto \llbracket M\rrbracket_{\rho[z \mapsto a, x \mapsto \llbracket N \rrbracket_\rho,y \mapsto a]})$

symplify

$(a \mapsto \llbracket M\rrbracket_{\rho[         x \mapsto \llbracket N \rrbracket_\rho,y \mapsto a]})$

by definition
$\llbracket \lambda y M \rrbracket_{\rho[x \mapsto \llbracket N\rrbracket_\rho]}$

\end{enumerate}



Some observations

Lambda-calculus doesn't specify what exactly $i$ is. We can suppose that $A_i=\emptyset$. Then
$A_{i\rightarrow i} = A_i^{A_i} = \{ \emptyset \}$ which is a set of size 1. $A_{(i\rightarrow i)\rightarrow i} = { \emptyset }$. i.e. cardinality $|A_{(i\rightarrow i)\rightarrow i} | = 0 $.

Do we have any other ways to construct $A_i$ to be able to construct lambda terms?

$\lambda$-calculus is a way to write intuitionistic proofs when we have logic with only implication. 
 $(\phi \rightarrow \phi)\rightarrow \phi$ is a tautology

But when we use empty set as $A_i$ we can get a \textit{classical} tautology which is not describably by $\lambda$-term.

\subsection{}
We need a one thing for completeness proof.

Completeness: If $\forall$ $A_i$ and $\forall$ $\rho$: $\sem{M}{\rho}$ then $M=N$ in 
$\alpha,\beta\eta$ sense.

Fridman's compeleteness theorem
If for $A_i=NN$ andnd all $\rho$: $\sem{M}{\rho}$ then $M=N$ in 
$\alpha,\beta\eta$ sense.

For finite set we can get lambda-terms which will not be $\alpha,\beta\eta$ equivalent. There is not enough room for terms.

It's rather difficult to proof Fridman's theorem straightforwardly.

\subsection{Henkin model for $\lambda$-calculus}
The idea is to select not the whole subset but a $A_{\sigma \rightarrow \tau} \subseteq {A_\tau}^{A_\sigma}$.

Let's define sematics for application:
$\sem{MN}{\rho} = \sem{M}{\rho}(\sem{N}{\rho})$.

$\sem{\lambda x . M}{\rho} = (a \mapsto \sem{M}{\rho[x \mapsto a]})$ which is $A_\sigma \rightarrow A_\tau$
The problem is that right part can be not in the chosen subset. And it's difficult to check this because the 
set has infinite size.

Let's suppose that $A_i$ is partially ordered set and
$A_{\sigma \rightarrow \tau} = \{ f: A_\sigma \rightarrow A_\tau | 
\forall x \leq y \in A_\sigma f(x) leq f(y)\}$
we take all monotone functions and in this case the problem does not occur (prove is an exercise).

At least the things we chosen should behave as functions, we need to be able to apply them.
$\forall \sigma, \tau app_{\sigma,\tau} : A_{\sigma \rightarrow \tau} \times A_{\sigma} 
\rightarrow A_{\tau}$

Extensibility: $\forall f,g \in A_{\tau \rightarrow \tau}$ $(\forall x \in A_{\sigma}: app(f,x) = app(g,x)) \Rightarrow f = g$, i.e. functions are the same if they behave the same.

$\forall \sigma,\tau$  $ab_{\sigma,\tau}: {A_\tau}^{A_\sigma} \rightharpoonup A_{\sigma \rightarrow \tau}$ (surjection).

$app (ab(f), x) = f(x)$

let $f: f: A_{\sigma} \rightarrow A_{\tau}, g \in A_{\sigma \rightarrow \tau}, 
(\forall x \in A_{\sigma} f(x) = app(g,x)) \Rightarrow ab(f) = g$

\section{Some notes about 1st day exercises}
\begin{itemize}
 \item 
 \item 
 \item Church typing: every var has a fixed type. Curry typing: terms are untyped, types are assigend
 The task was too typecheck $TT$ where $T=\lambda f \lambda x f(f(f x))$. The answer is 
 $(\alpha \rightarrow \alpha) \rightarrow (\alpha \rightarrow \alpha)$.
 
\begin{prooftree}
\AxiomC{$f$}
\AxiomC{$x$}
\BinaryInfC{$f x$}
\AxiomC{$f$}
\BinaryInfC{$f (f x)$}
\AxiomC{$f$}
\BinaryInfC{$f(f(f x))$}
\UnaryInfC{$\lambda f^3 x$}
\UnaryInfC{$\lambda f \lambda x f^3 x$}
\end{prooftree}
... and long exlanation about Milner's type reconstruction alrorithm, occurs check and that 
$A \neq a \rightarrow B$ for any \textit{finite} $A$.

Exercise 4.
$A_i$ is o.o. set. 

%TODO

Lemma. $x \leq y$, $f \leq g$ then $f(x) \leq g(y)$.  Proof. let's put $f(y)$ in the middle



Now 
$\sem{\lambda x . M}{\rho}$ = $(a \mapsto \sem{M}{\rho[x \mapsto a]})$ 

$a \leq b$ : $\sem{M}{\rho[x \mapsto a]} \leq \sem{M}{\rho[x \mapsto b]}$

by induction of the structure of M.

Application: $M \equiv x$ $M\equiv y$ $M=NP$

$\sem{M}{\rho[x \mapsto a]} \leq \sem{N}{\rho[x \mapsto b]}$ 

Lambda-abstraction:
$M = \lambda y . N$, $\sem{\lambda y N}{\rho[x \mapsto a]} = (c \rightarrow \sem{N}{\rho[x\mapsto a, ]})$

$\rho \leq \rho' if \forall x \in Var \rho(x) \leq \rho'(x)$

$\sem{M}{\rho} \leq \sem{M}{\rho'}$ And now a random question where we use antimonotonicity for ordered relation 
which nobody did get.


\end{itemize}


\section{DAy 2}
Back to completness proof. Now we will chose only one model and only one $\rho$ to show 
$\alpha, \beta, \eta$ equivalence. The general technique is to make a completness proof for a new caculus 
to be sure that we listed enough rules in it.

Termmodel: $S_\sigma = $ all terms of type $\sigma$ $ / \alpha\beta\eta$. So we introduce equivalence classes.

$[x^\sigma] \in S_\sigma$. Also $(\lambda x .x) x$ is in the same class, so $S\sigma$ is infinite. 
$[y^\sigma]$ is another class,


$\forall \sigma |S_\sigma| $ is countable but infinte.

$app([M],[N]) = [MN]$ by definition.

in case when $[M]=[M']$ and $[N]=[N']$ we need to prove that $app([M],[N]) = [M'N']$

We had a rules
\begin{prooftree}
 \AxiomC{$ M=M'$ in $\alpha\beta\eta$ sense}
 \AxiomC{$ M=N'$ in $\alpha\beta\eta$ sense}
 \BinaryInfC{$ MN=M'N' $ in $\alpha\beta\eta$ sense}
\end{prooftree}


% И тут вопрос от Вяткина, который никто не понял кроме препода
% Напомнить Диме что-то меня спросить про офис где-то

Showing extensionality.  When we ouck two functions from same class, and if they behave same
they should be equal.

$[M], [M'] \in S_{\sigma \rightarrow \tau}$
Assume that $app([M],[N]) = app([M'],[N]) \forall [N]\in S_{\sigma}$. We need to show that $[m]$ and $[M']$ 
are $\alpha\beta\eta$-equal. We will use particular $[x^\sigma]$ for $[N]$. 
Now $[Mx] = [M'x]$ are the same or
in another words $Mx = M'x$ are $\alpha\beta\eta$-equal. By congruence rules we can add $\lambda$: 
$\lambda x M x = \lambda x . M' x$ 
and $M$ is $\eta$-equal $\lambda x . M x$ 
and the same for $M'$. We suppose that 
$x$ doesn't occur in $M$ and we need a right to choose right $x$ (there we use that the sets are infinite).

Now something less trivial.

$\rho: Var \rightarrow \cup S_\sigma where \sigma is a type$


$\sem{\lambda x . M}{\rho}$ = $([N] \mapsto \sem{M}{\rho[x \mapsto [N]]}$, Now the right part should 
have a representative that behaves in the same way $\in S_{\sigma \rightarrow \tau}$. which is almost trues except the free vars in $M$
.

Claim. I can compute sematics in the different way. For any term $M$ and any $\rho$
$\sem{M}{\rho} = [M[r]]$ where ($r$ is a \textit{simultanious} substitution)
for each $x$ $r(x) \in \rho(x)$



Now exercise about about defining an simultanious substituion. the proplem was that people 
think substitution as finite-defined function from free variables in term. In math substituition is 
usually defnied as global function that behaves everywhere, and behaves as identity for variables 
that do not occur free in the specified term

Definition.
$x[r] = r(x)$

$(MN)[r] = (M[r])(N[r])$

$(\lambda x . M)[r] = \lambda z . M[r, x \mapsto z] $ where $z \not\in  FV(r(y)) for y \in FV(M)$

Simultaneous menas that we do not do full substitution, we are not going to introduce closed terms,
we only do the first level.

Proof of claim.
$M\equiv x    \sem{x}{\rho} = \rho(x)$ and $[x[r]] = [r(x)]$ and now $\rho(x) = [r(x)]$ bceause 
$r(x) \in \rho(x)$, $[r(x)] = \rho(x)$.

Lambda case is long....
$M=\lambda x . M$, $\sem{\lambda x . M}{\rho}$ = $([N] \mapsto \sem{M}{\rho_{x \mapsto [N]}})$
  
$[(\lambda x . M)[r]]$ = $[\lambda z . M[r, x:= z]]$. Now we need to look what happen when we apply
$[\lambda z . M[r, x:= z]]$ to $([N] \mapsto \sem{M}{\rho_{x \mapsto [N]}})$.

$app ([\lambda z . M[r, x:= z]], [N])$ = $[(\lambda z M [r, x:=z])N]$

 = $[(M[r, x:=z])[z:=N]]$
 
 because z is completely new 
 
 = $[M[r, x := N]]$. Now we should show that $r$ should match the environment. The only change we done
 is $x$ to N. And by induction hypothesis the $[M[r, x := N]]$ is $\sem{M}{\rho_{x \mapsto [N]}}$.
 
We did something but did not use $\alpha$ equivalence. It means that it is redundant. Exerceise to prove it.
(5 minutes later is not sure about it btw)

$\sem{M}{\rho} = \sem{N}{\rho}$ for $g(x)=[x]$ ($r(x)=x$).

 $[M]$ = $[[M[r]]$ = $\sem{M}{\rho} = \sem{N}{\rho}$ =  $[[N[r]]$ = $[N]$.
 
 and now $M=N$ in $\alpha\beta\eta$-sense.


  
\subsection{maybe something about logical relations}
Let we have $A_i$ and $B_i$ and we want to relate model based on natural numbers

$R_i \subseteq A_i \times B_i$

$R_{\sigma \rightarrow  \tau} = \{$ (f,g) $\in A_{\sigma \rightarrow \tau} \times
B_{\sigma \rightarrow \tau} |
\forall (x,y) \in R_\sigma (f(x), g(y)) \in R_\sigma \}$

Fundamental lemma for logical relations.
for any type $\sigma$, for any closed term $M$ of type $\sigma$ it's true that 
$(\sem{M}{} ^A, \sem{M}{} ^B) \in R_\sigma$

Proof. INduction over structure of general terms.

Notes. This lemma is true not only for set-theoretic model but also for Henkinmodel andnd
others.
let term is a variable. $(\sem{x}{\rho_A}^A, \sem{x}{\rho_B}^B) \in R_\sigma$

$\sem{x}{\rho_A}^A$ = $\rho_A(x)$
$\sem{x}{\rho_B}^B) = \rho_B(x)$

We can't take any $\rho$'s but any $\rho_A$,$\rho_A$ that $\forall x (\rho_A(x), \rho_b(x)) \in R_\sigma$.


% after lunch continuation
A: full ($A_{\sigma \rightarrow \tau} \subseteq A_{\tau}^{A_\sigma}$) set-theoretic model over $N$.

B: term model.

logical relation : $R_i \subseteq A_i \times B_i = N \times S_i$ such that $R_i$ is a surjective 
function from N to $S_i$\footnote{There we use that N is countable}.

Claim. For all types $\sigma$, $R_\sigma$ is a partial surjective function from $A_\sigma$ to $S_\sigma$.

\begin{itemize}
 \item $(a,t) \& (a,t') \in R_\sigma \Rightarrow t = t'$
 \item $\forall t \in S_\sigma \exists a  \in A_\sigma (a,t) \in R_\sigma$
\end{itemize}

Proof. Induction over all types .

$i$: OK, by assumption.

$\sigma \rightarrow \tau$ : $R_\sigma$,$R_\tau$ are partial surjective functions. Let's show 
$R_{\sigma \rightarrow \tau}$ has properties 1 and two.

% картинка из теорката.
%\begin{equation}
\begin{tikzcd}
A \arrow [ r , ''f'' ]
%  \arrow [ dr , swap , '' g \circ f'' ]
  &
B 
%  \arrow [ dr , '' g \circ h '' ]
%  \arrow [ d , swap , '' g '' ]
%  \\
%  {}
  &
C %\arrow [ r , swap , '' h '' ]
%  &
%D
%  &
\end{tikzcd}
%\end{equation}

% Продолжение каринки.

Need $(f,m) \in R_{\sigma \rightarrow \tau})$. Let $(A,t) \in R_\tau$

$(f(a), m(t)) = (S_\tau(R_\sigma(a)), m(t))$ = $S_\tau(m(t)), m(t)) \in R_\tau$

Now proof of Friedman's theorem.
$\sem{M}{\rho}^A = \sem{N}{\rho}^A$

Chose $\rho$: $\forall x \in Var      [x]_{\alpha\beta\eta} \in S_\sigma$
And because the logical relation is surjective  we can choose $\rho$ that

$(\rho(x), [x]_{\alpha\beta\eta}) \in R_\sigma$. We could write
$(S_\tau([x]_{\alpha\beta\eta}), [x]_{\alpha\beta\eta}) \in R_\sigma$.


$( \sem{M}{\rho}^A, \sem{M}{\rho'}^B ) \in R_\sigma$
     ||
$( \sem{N}{\rho}^A, \sem{N}{\rho'}^B ) \in R_\sigma$     

where $\rho'(x) = [x]_{\alpha}$ and now

$[M] = \sem{M}{\rho'}^B = \sem{N}{\rho'}^B = [N]$. So, $M=N$ in $\alpha\beta\eta$-sense. Qed.

There is a similar theorem in the model-view calculus (or maybe $\mu$-calculus, my hears are bad.).


\subsection{more about logical relation}

$(\sem{M}{}^A, \sem{M}{}^B) \in R_\sigma$

We could also set fundamental lemma for unary relations and single model.
$\sem{M}{} \in P_\sigma$ ($P_i \subseteq A_i$, $R_i \subseteq A_i \times B_i$). we can relate $A_i$ to himself
and get $(\sem{M}{}, \sem{M}{}, ..., \sem{M}{}) \in R_\sigma$ where $R_i \subseteq A_i \times A_i \times A_i \times ... A_i$.

Definition. $A\in A_\sigma$ is invariant of $(a,a,a,a,,.....a) \in R_\sigma$ for any logical relation $R$.

Fund. lemma. the semantcs of closed $\lambda$-term is invariant.

Question. Is every invariant element the Semantics of a closed term?   

No.

Propostition. (plotkin, 80). a $\sigma$ is a type of order 2. $A_i$ is an infinite set. Every invariant  
elment of $A_\sigma$ is $\lambda$-definable.

$ord(i) = 0$ and $ord(\sigma \rightarrow \tau) = max { ord(\sigma) + 1, ord(\tau)}$

The proof for >2 we need ''improved logical relations``. But there is a paper about it.

Theorem [Loader`93]. The $\lambda$-definability problem is undecidable.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{day 3}

Now we will got closer to computers and computable functions.

Some historic perspective.

Computable functions: $N \rightharpoonup N$ (Turing). Only nubers matters.

In 1950s we got Fortran. In 1956 Algol community firstly met, Algol58 was the academic language,
the Algol60 became 1st public knowing language. Algol68 become less pwerful than Algol60.
Formal description of the language was semantics and denotational semantics is one of approaches.

Stratchey, Landin: denotational semantics  as translation into untyped $\lambda$-calculus.
Dana Scott knowed all the problems of untyped lambda calculusbut still lambda-calculus was not 
completely unreasonable. But Scott still said that it is not right to convert something to the 
thing you can't understand. STLC is OK in this question but is not suitable for writing computable 
functions. So he extended it to LCF. Initially he did not know that will be treated as a language.

Scott (69): typed lambda calculus
Plotkin(76): LCF considered as a programming language.

LCF -- Logic of Computable Functions.

PL language converted with this approach is known as PCF but it was known as language wher ewe give 
names to set-theoretic functions. The theory of recursion was alrady very sophisticated but
Scott's approach is original: defining functions in domains.

% Platek had a thesis about recursion. It was very sphisticated and ungooglable.

\subsection{PCF}

Types: $\sigma ::= bool | i  | ...$ (where $i$ is $\iota$). The $\iota$ was initially for ''individuals``
but people think that as numbers (natural or real).

$\sigma ::= bool | i | \sigma -> \sigma$.

Terms: Scott added logical types (for bools) and other types (where for example axioms about successor
depend on the choice of $\iota$).

Terms: $M ::= x | MM | \lambda x . M | If: bool -> \sigma  -> \sigma  -> \sigma | .... $

Also $|succ | pred | zero? |...$ for logical types. And he said that ''he can't add assignment to language" :)

So he added $ | Y $.

The type of Y-combinator : $Y_\sigma : (\sigma \rightarrow \sigma) \rightarrow \sigma$.


There were names in the PCF, so we can't write \verb=let rec ...=. That's why we need Ys-combinator.

Also we need $... | \\ff | \\tt | 0$ as terms

Now we declare rewrite rules as Plotkin did (It is very brief description, which can be not full
and contain errors both because the lecturer bieleved that we all know this stuff and that
the function between what he said and \LaTeX    sometimes returns $\bot$.

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{zero? $0 \rarr \tt$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{if $\tt M N \rarr M$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{if $\ff M N \rarr N$}
\end{prooftree}


\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ P \rarr P'$}
 \BinaryInfC{if $P M N \rarr if P' M N$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ P \rarr P'$}
 \BinaryInfC{$ zero? P \rarr zero? P'$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ M \rarr M' $}
 \BinaryInfC{$ MN  \rarr MN'$}
\end{prooftree}

Call-by-name as in Haskell:
\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{$ (\lambda x . M) N \rarr M[N/x]$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{$zero? (k+1) \rarr \ff$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{$ YM \rarr M(YM)$}
\end{prooftree}

\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{$succ$ $k \rarr k+1$}
\end{prooftree}

There we do not reduce under lambda because we do not have congruence rules.

Now and example of a factorial to demonstrate that the order where we apply reductions matter.
\begin{verbatim}
letrec f = \x -> if zero? x then 1 else f(pred x) * x

we will write `\x -> if zero? x then 1 else f(pred x) * x` as M
Y(\f  \x -> if zero? x then 1 else f(pred x) * x ) : (int->int) -> (int->int)

Y(\f . M(f)) 2
(\f . M(f)) (Y(\f . M(f))) 2
now \beta step
M[Y(\f . M(f))] 2
\beta
if zero? 2 then  1 else (Y(\f . M))(pred 2) * 2
\end{verbatim}

Let's look at $Y_{int}: (int\rarr int) \rarr int$. Let's evaluate application of $Y$ to $succ$:
$succ (Y succ)$, $succ (succ (Y succ))$, ... and recursion to infinity. 
But we know that to get complete calculus we need to allow partial 
functions. So we do not say here about total functions.

\paragraph{}
Semantics of types: $\sem{bool}{} = \{\tt, \ff\} = B$, $\sem{int}{} = \{0, 1, ...\} = N$.

Sematics for terms : $\sem{M}{\rho} $ as before

$\sem{zero?}{} \in B^N$

$\sem{YM}{} = \sem{M(YM)}{} = \sem{M}{} (\sem{YM}{})$
Observation, $\sem{YM}{}$ must be a fixpoint of the $\sem{M}{}$. $Y$ should produce fixpoint for every 
definable functions. $Y$ of identity exists but $Y$ applied to $succ$ did not converge.

%%%%%%%%% some questions about primitive recursion vs. Y-combinators

And about $\mu$-recursion.
 \[
    g(a_1,...,a_n)=\left\{
                \begin{array}{ll}
                  \text{min } n\in N, \text{s.t.} f(n,a_1,...,a_n)=0\\
                  \text{undefined else}
                \end{array}
              \right.
  \]
  
  
  
%$g(a_1,...,a_n) = \mu f = \Big\{ \frac{min n\in N, s.t. f(n,a_1,...,a_n)=0}{undefined else}$

Exercise to express $\mu$ in PCF.
Solution.
\begin{verbatim}
 let rec min = \f . \x . \a . if zero? f x a then x else min f (succ x) a
\end{verbatim}
% Но я не понял почему f от 0 завершается. То ли она тотальна, то ли примитивно-рекурсивна.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{}
Now we will try to define semantics for PCF.
We kind of need to have an element to denote ``no value''. We will call it bottom: $\bot$.

bool :   true  false
           \    /
            $\bot$
            
\paragraph{}
Now we will describe functions in $\sem{bool}{}$ which have 27 functions (as functions from 3
element set to 3 element set). But we do not want semantics to explode. We want to say that 
many functions are not realistic and we do it by adding order to the set. Let's describe 
\textit{monotone} functions in this set .

% we use derivations trees to draw a graph

$\sem{bool}{} = B_\bot$

Now for natural numbers. Picture.

$\sem{int}{} = N_\bot$ 

The only way to define succ OK is when $\bot$ goes to $\bot$ because of monotonicity. Let's call
functions that goes from $\bot$ to $\bot$ as \textit{strict}.

Now 
$\sem{int \rarr int}{}$ has infinitely many and uncountable. That means that there some functions
in semantics that are undefinable. In STLC we get infinite in the power of infinity, etc... (terrible 
infinity) but in PCF the infinity doesn't grow (This is respect to PCF and not to domain theory otself).

Let's look at partial function $f: N \rightharpoonup N$ we can alsways convert it got 
$f': N_\bot \rightharpoonup N_\bot$. What the order will be here?

%  тут не штрихи, а черты сверху

$ f \leq g: \forall x f'(x) \leq g'(x)$

iff $f(x) = g(x)$ or $f(x)=\bot$. One function is better than another when ot is mpre defined that
the other. But if function below is defined we can't change values.

$c_\bot \leq \{0\mapsto 0; else \bot\}
        \leq \{0\mapsto 0; 1\mapsto 1; else \bot\}
        \leq .....
        $
        
Now let's look at F: $(int \rarr int) \rarr something$, for example        
$(int \rarr int) \rarr int$. First argument is all monotone functions. It also should be monotone,
so ``if you give me better function, I will give you better result''.

Now how we define it? If we are gotten a rubbish function $(\bot \rarr\bot)$ we can only return 
just a value (say $5$). But if we get good function, we trust it and execute it so
we can execute it only finite number of times (unless we diverge). So we will only use values of the 
argument function only on finite number of inputs.  So, we do not need to go to the top of the 
sequence above. I.e. in any HOF argument is used only finite number of times.
        
So, the $F$ is computable only if following is true:
chain $f_0 < f_1 < f_2 < ...$ will always limit the use of f: 
$lim F_n where n\in N = V f_n where n\in N$

% здесь не V а большая галка со стрелкой вверх в правой ветке.

So, if Ff returns a value, it was defined on the chain.

Def. F is Scott-continious if for all chains  $f_0 < f_1 < f_2 < ...$
the $V F(f_n) = F(Vf_n)$ for all n$\in N$.
\begin{definition}{Scott-continious.}
F is Scott-continious if for all chains  $f_0 < f_1 < f_2 < ...$
the $V F(f_n) = F(Vf_n)$ for all n$\in N$.
\end{definition}
N.B. it can be $\leq$ in the chain but it will make more difficult reasoning. There we
the notion of непрерывности but for isolated input.

Def. (D, $\leq$) is CPO (complete partial order) if for every chain $a_o \leq a_1 \leq ...$
there is a limit $a$: $a_n\leq a$ for every $n$ and for every $b\in D$: $a_n\leq b$ $a\leq b$ .
and there is a least element $\bot_D$.

We had the same for $R$: supremum:

So the function $F: D \rarr E$  (where $D,E$ are CPOs) is Scott-continious 
if it is monotone and for all chains  $f_0 < f_1 < f_2 < ...$
the $V F(a_n) = F(V a_n)$ for all n $\in N$.

So, we restricted monotone function to continious ones. 

We did all of that because of we didn't get a fix-points in the original model. Let's do this.


\begin{theorem}
$D$ is CPO and $f: D \rarr D$ is Scott-continious . Then $f$ has a least fixpoint.
\end{theorem}
\begin{proof}
$\bot \leq f(\bot)$. Now we apply $f$ to both sides, and order will be preserved.

$f(\bot) \leq  f(f(\bot))$. So we get a chain
$\bot \leq f(\bot) \leq f(f(\bot)) \leq f(f(f(\bot))) \leq ....$. Because CPO

% Мы можем рисовать кубы тут.

there is a limit of this sequence. $a = Vf^n(\bot)$ where $n\in N$. 
Claim1: $a$ is a fixpoint of $f$.
Claim2: it is a least fixpoint

Let's proof claims.

$\bot \leq f(\bot) \leq f^2(\bot) \leq f^3(\bot) \leq ... Vf^n(\bot)$

$f(\bot) \leq f^2(\bot) \leq f^3(\bot) \leq f^4(\bot) \leq ... Vf^n(\bot)$

$f(Vf^n(\bot)) = Vf^{n+1}(\bot) = VF^n(\bot)$

Now proof claim2:
 
 $\bot \leq a = f(a)$
 $f(\bot) \leq f(a) = a$.
 $f^2(\bot) \leq a$.  So we showed a fixpoint which is a least fixpoint.
.
\end{proof}

$\sem1{Y}$ where Y has type $(\sigma\rarr\sigma)\rarr\sigma$,
$\sem1{Y} = (f \mapsto V f^n(\bot)$

All that we done we have done in a theoretical way without knowledge about PCF. Now we
should stuck in monotone functions and in CPOs.

Some long speach about there are very low count of categories that are with this properties.

End of the day 3.


Some exercises explantations

\begin{itemize}
 \item 
 \item $f = M (f, g) : \sigma \rarr \tau$
 
 $g = N(f,g) : \sigma' \rarr \tau'$
 
 $Y_{\sigma' \rarr \tau'} (\lambda g . N)$
 
 $Y_{\sigma \rarr \tau} (\lambda f . M[Y(\lambda g . N) / g])$
 \item (a) ($N^T$)There is not natural number.
   (b) Is because something about zero...
   (c) NO, because approximation of $\sqrt{2}$ has no least upper bound.
   (d) Yes
 \item 1st aprt is obvious.
 \item $f:D \rarr D$, $\bot \in D$ ccpo.
 
 $C \subseteq  D$ is a chain  if $\forall x,y \in C$: $x \leq y$ or $y\leq x$.
 
 Let's look at $\bot \leq f(\bot) \leq f(f(\bot)) \leq ...$ $Vf^n(\bot) = l_1$

 $f(l_1) \leq f(\bot) \leq f(f(\bot)) \leq f(f(f(\bot))) \leq ...$ $Vf^n(\bot) = l_2$
 
 $V l_n = l_\omega$ for $n\in N$. Now we do  sequence for $l_i$. 
 %When we continue this  process for all 
 Set theory says that we can't go strictly up,  so we will hit $a=f(a)$. Is it a least fixpoint?
 $b=f(b)$. Look: $\bot \leq b$ and $f(\bot) \leq b$ .... etc. So we conclude that 
 $V f^n(\bot) \leq b$. Wo we have a least fixpoint $a$.
 
 Now an artifictial exampele where f of limit is not a limit of fs. Int topology the 
 open intervals has a limit as closed interval. In Reals it is OK, but we can invent some topologycal
 shit where lengths doesn't work in this way.
 
 Dino Pataraia. with Escado has a paper with some proof don't sure about what.
 
 \end{itemize}

 
\section{Day 4} 
Yesterday we switched from sets to sets with bottom attached (to have in Y-combinator 
for every function, which is not possible in the STLC).
we have $N_\bot$ and $B_\bot$ which are both infinite but without interesting chains.

% REmembering the definition of continiousity and that every continious function has a least fixpoint.
Now we have least fixpoint (lfp) that has type $[D\rarr D] \rarr D$. Is lfp itselft continious.
The best thing to think about it is category theory.

Cathegory CPO: objects are all CPOs, morphisms are continious functions.

To switch to Henkin model we need a requirement that category is cartesian-closed.

\begin{theorem}
Lemma. CPO is cartesion-closed. 
\end{theorem}
\begin{proof}
 \textbf{Concrete} product  $D\times E$ is a cpo. $(d,e) \leq (d',e') if d\leq d' and e\leq e'$.
 
 Bottom $(\bot_D,\bot_E)$ $V(d_n,e-_n) = (Vd_n,Ve_n) for n \in N$

 % A remark that Product of everything ffrom empty set is 1.
 
 $[D\rarr E]$   $f\leq g$ if $\forall d in D$ $f(d) \leq_E g(d)$
 
 $\lambda x . \bot_E$.
 
 $(V f_n)(d) := Vf_n(d)$.
 
 % Картинка от Вяткина. Про то, что в матане теорема неверна, потому что там мы ожидаем 
 % чтобы лимиты слева и справа были одинаковыми. А тут мы всегда приодим слева.
 $(V_nf_n)(V_md_m) = V_nV_m f_n(d_m) = V_mV_n f_n(d_m) = (V_mf_m)(V_nd_n)$
\end{proof}
 
 --------------------
 
 $f: D \times E$ is continious iff f is componentwise continious $f(Vd_n, e) = Vf(d_n,e)$.
 
 Application: $f: [D \rarr E] \times D \rarr E$ is continious.
 
 $app 9vf_n,d) = (Vf_n)(d) = Vf_n(d) = Vapp(f_n,d)$ which again magically works but in 
 analysis functions continious componentwise can be not globally continious.
 
 --------------------

 curry(ab): $[D\times E \rarr F] \rarr [D\rarr [E\rarr F]]$.
 
 ------

 composition: $[D\rarr E] \times [E \rarr F] \rarr [D\rarr F]$.
 
 
 Now we need to show that we have Henin model here and this folows abstractly from that we  have... ?
 
 lfp continious
 
 $lfp(f) = V f^n(\bot)$
 
 $lfp_n(f) = f^n(\bot)$ and $lfp = Vlfp_n$. let's show that $lfp_n$ are continios by inductions.
 
 $lfp_0(f) = \bot$, $lfp_{n+1} = app(f, lfp_n(f))$
 
 
 Back to lambda calculus.
 
 $\sem{succ}{} : N_\bot \rarr N_\bot $ and others are cpo's. The fact that lambda abstraction is
 show follow from that it is cartesian closed.
 
 $\sem{x}{\rho}$, $\sem{MN}{\rho} = app(\sem{M}{\rho}, \sem{N}{\rho})$.
 
 $\sem{\lambda x.M}{\rho} = (a \mapsto \sem{M}{\rho[x \mapsto a]}) $is continious.
 
 Let's vary some component: $b_n \mapsto \sem{\lambda x.M}{\rho[y\mapsto b_n]} = 
 (b_n \mapsto (a \mapsto \sem{M}{\rho[y\mapsto b_n][x \mapsto a]})) $ now we use curry/uncurry to change 
 $(a \mapsto (b_n \mapsto \sem{M}{\rho[y\mapsto b_n][x \mapsto a]}))$
 
 $E\rarr[A\rarr F]]$ uncrurring to $[E\times A]\rarr F$ changing order $[A\times E]\rarr F$ and 
 curring  to $A\rarr[E\rarr F]]$
 
\begin{theorem}
 CPOs and Scott-continious functions provide a correct denotational semantics for PCF,
 i.e. if $M\rarr M'$ then for any env. $\rho$ : $\sem{M}{\rho} = \sem{M'}{\rho}$.
\end{theorem}
There functions are equal if they behave equal. Folks tried to extend domain theory to 
comlexity issues but not really succeed.

\begin{proof}
 Just go through all rules and check for everyone.
\end{proof}

Here we do not expect completness (i.e. theorem do not work in the opposite way), because it will 
be mean that we can rewrite merge sort into quick sort by rules, but this two algoritms are completely
different algorithms.

The $\sem{\cdot}{}$ is adequate, if $\forall$ closed terms of ground type, $\sem{M}{}=n$ then
$M \rarr* n$ in finitely many steps. D.Scott couldn't answer this question. Plotkin did it 8 years 
laters.

\begin{proof}
 At \underline{int}: $a R_int M$, where $M$ is closed and of type \underline{int}.
 
 if $a = \bot$ or $a=n$ then $M \rarr *n$.
 
 Adequacy: $\sem{M}{}R_{int}M$. Now we show 4 properties of this relations to get to fundamental lemma.
 
 \begin{enumerate}
  \item $\bot_\sigma R_sigma M:\sigma$ always.
  
  $f R_{\sigma\rarr \tau}M$ iff $\forall a R_\sigma N$, N closed and of type $\sigma$:
  $f(a)R_\tau MN$. PCF is   reach and we can not to go to open terms.
  
  Proof.
  
  $\bot_{\sigma\rarr \tau} R_{\sigma\rarr \tau}  M : \sigma \rarr \tau$
  %\begin{DisplayProof}
   %???
  %\end{DisplayProof}
  Qed.
  \item [Step 2]
  $aRM$  and $M'\rarr M$ them $aRM'$. when $a=\bot$ it is in relations. When $a$ is a number
  then $M'\rarr M\rarr .... \rarr n$. For function type : we have $fR_{\sigma\rarr \tau}M'$ and
  $aR_\sigma N$ we need to show $f(a) R_\tau M'N$. easy: $f(a)R_\tau M'N \rarr f(a)R_\tau MN $
  \item[Step 3] 
  if we have sequence chain $a_n$ and $a_nRM$ then $Va_n RM$.At ground type we do not have any 
  chains, nothing interesting happend. Let's look at function type: 
  $f_nR_{\sigma\rarr \tau}M \Rightarrow Vf_nRM$.
  
  $f_n(a)R_{\sigma\rarr \tau}MN$,  $(Vf_n)(a) = Vf_n(a) R_\tau MN$.
  
  \item [Step 4]
  Need to show that for all types $\sigma$ and all $M:\sigma$: $\sem{M}{}R_\sigma M:\sigma$.
  Wel will proof slightly stronger statement about open types.
  
  $\rho$, $r$ (substitution with closed terms) such tath for $\forall x$: $\rho(x)Rr(x)$, i.e.
  $\sem{m}{\rho}R M[r]$ -- this what we are trying to show. Variable case simple. Application and
  abstraction are similar to $\lambda$-calculus. The interesting cases are constants and $Y$-combinator.
  
  $m=succ N$. We assume them $\sem{M}{\rho}RN[r]: int$.
  
  $succ\sem{N}{\rho} = \sem{succ N}{\rho}$ and going to show $\sem{succ N}{\rho} R succ N[r]$.
  case 1: $\sem{N}{\rho}=\bot$. case 2: $\sem{N}{\rho} = n$ then $N[r] \rarr * n$ then 
  $succ(N[r]) \rarr* succ(n) \rarr n+1$. There we used rule for successor.
  
  Now we going to show that $\sem{Y}{}R_{(\sigma\rarr\sigma)\rarr \sigma}Y_\sigma$. Need to test
  this of some $f$,$N$:that $fR_{\sigma\rarr\sigma}$ and need to show that $lfp(f)R_\sigma YN$.
  $\bot_{\sigma}R_\sigma YN$, $f(\bot_\sigma)R_\sigma N(YN))$, and $f(\bot)R_\sigma YN$ and by 
  induction $f^n(\bot)R_\sigma YN$  and now take supremum: $V f^n(\bot)R_\sigma YN = lfp(\bot)$
  
 \end{enumerate}

\end{proof}

we introduced order to get fixpoint but now we going to say that matter. Let's say that
$M \lesssim_{c} M'$ when every programmer will take $M'$ instead of $M$, i.e.
if $\forall C[]$ (ground) context $c[M] \rarr*n$ $\Rightarrow C[M']\rarr*n$. We will 
cal it ``contextual preorder''.

Want (full abstraction lemma): $M\lesssim_c M'$ iff $\sem{M}{} \leqslant \sem{M'}{}$. ``Fully abstract'' semantics.
The Scott's semantics is not. Today we will show that right to left direction holds.

\begin{theorem}[Test-Context Lemma]
 $M \lesssim_c M': \sigma$ iff $foral P: \sigma \rarr int$: ($PM \lesssim_c PM'$ iff
 ($PM \rarr * n \Rightarrow PM' \rarr* n$).
 
\end{theorem}
--------------------
\begin{proof}
 down $C[] := P[]$, up $C[] \rightsquigarrow \lambda x. C[x]=:P$
\end{proof}

 Proof of lemma.
 $\sem{M}{} \leqslant \sem{M'}{} \Rightarrow M \lesssim_c M'$.
 
 if $PM \rarr * n$ then $\sem{P}{}(\sem{M}{}) = \sem{PM}{}=n$. but 
 $\sem{P}{}(\sem{M}{}) \leqslant \sem{P}{}(\sem{M'}{}) = n = \sem{PM'}{}$. Now by adequacy we have 
 $PM'\rarr* n$.

\begin{theorem}[Context Lemma (Milner 78)]
 The following are equivalent for closed terms $M$,$M':\sigma$.
 \begin{enumerate}
  \item $M\lesssim_c M'$
  \item $M \rarr M'$ in applicative context : we view them as functions and test them on arguments.
  $MN_1N_2N_3 .... \rarr * n$ and $M'N_1N_2N_3 \rarr * n$.
  \item $\sem{M}{}RM'$.
 \end{enumerate}
\end{theorem}
\begin{proof}
 \begin{itemize}
  \item $1\rarr 2$ should be easy.
  \item $2\rarr 3$. $\sem{M}{}RM$, $a_iRN_i$. waht $\sem{M}{}(a1)(a_2).. R_{int}MN_1N_2$. If left
  is equal to bottom then finished. Else It converges in finitely many steps to numeral. By ass(2)
  right part also converges to numeral
  \item $3\rarr 1$. Want $PM \lesssim-c PM'$, by fund. lemma $\sem{P}{}RP$. and by definition of logical
  realtions  $\sem{PM}{}R_{int}PM'$. If $PM$ converges to number thein finitely many steps to number
  then $\sem{PM}{}=n$ and by definition of ?? $PM' \rarr * n$.
 \end{itemize}

\end{proof}

Scott's model fails to be fully-abstract because there some stuff in the model that is not definalbe.
In $bool\rarr bool$ everything is definable but in $B_\bot^2\rarr B_\bot$ not.
Let's look at ``parallel or`` (\verb=pr=).
$por(\ff,\ff) = \ff$,
$por(\ff,\bot) = \tt$,
$por(\bot,\tt) = \tt$,

Observation: There is not PCF term that implements por.
\begin{proof}
 if PCF could do this it will be in Java
\end{proof}

The test for parallel or: $portest_{a,b} : (bool^2\rarr bool)\rarr int$. returns $a$ if it is, $b$
when not and can diverge. Any two portests are equivalent. $\Omega$ means infinite loop.

$\lambda p . if p(\ff,\ff) then \Omega else if p(\tt,\Omega) 
    then if p(\Omega,\tt) then a else \Omega
    else \Omega$
    
Por always returns $\bot$    unless we give it parallel or. In practive they all  will be $\bot$.
But in semantics parallel or exists.

Question: por is $\mu$-recursive but why we can't rewrite it in PCF. The difference is between 
turing computation an typed computation, turing machine works on numbers.

One more theorem for that day.

\begin{theorem}[Plokin 77]
 PCF + parallel or is fully abstract for the Scott model.
\end{theorem}
Can we independently from PCF in Scott's model decide what is computable and what is not?
\begin{theorem}[Plotkin,77]
 PCF+parallel or+parallel exis is computationally complete.
\end{theorem}
Parallel exists has type : $(int\rarr bool) \rarr bool$ and 
$p.ex (\lambda x . \ff) = \ff$, and
$p.ex (g) = \tt$ if exists $n: g n = \tt$


Day 5

Exericses explanation.

\begin{enumerate}
 \item 
 \item 
 \item 
 \item $M\lesssim_c M' $ iff $\forall C[]: int: C[M] \Downarrow n \Rightarrow C[M'] \Downarrow n$
  Lemmma. T.f.a.e
  \begin{enumerate}
  \item[1] $M \lesssim_c N$
  \item[2] $\lambda x_1 .... x_k M \lesssim_c \lambda x_1 .... x_k M'$
  \item[3] $\forall P: ((\bar\tau \rarr \sigma) \rarr int$ 
  $P(\lambda x_1,...,x_n . M) = P(\lambda x_1,...,x_n . M')$
  \item[2\' by Razplohas] $\forall \tau: Var \rarr PCF_0: M[r] \lesssim_c M[r']$
  \item[3\' by Razplohas] $\forall P:\sigma \rarr int: PM[r] \lesssim_c PM[r']$
  \end{enumerate}
  
  Begin proof.
  (1)$\Rightarrow$(2). 
  Want: $C[\lambda \bar{x} . M] \lesssim_c C[\lambda \bar{x} . M']$.
  $D[]:=C[\lambda \bar{x}. []]$
  
  (2)$\Rightarrow$(1). 
  Want: $C[M] \lesssim_c C[M']$. We going to create context of more complex type.
  $D[] := C[ []_{\tau_1\rarr\tau_2\rarr ..\rarr\tau_k\rarr\sigma} x_1 x_2... x_k]$.
  In $D[\lambda\bar{x}.M] = C[(\lambda\bar{x}.M) \bar{x}]$ after $\beta$-step beocmes $C[M]$.
  
  (2)$\Leftrightarrow$(3) is just old lemma because we are talking about closed terms.
  (2)$\Rightarrow$(2') 
  Want $C[M[r]] \lesssim_c C[M'[r]]$, $N_i = r(x_i$ and $D[]:=C[[]N_1 N_2 ... n_k]$.
  
  
  Also (3'') $PM \lesssim_c PM'$ should be ok, but it is less useful because $PM$ still can contain 
  free variables and we can reduce it to number.
  
  (2') to (2). Instead of going directly we go to applicative order. I.e. we can apply cosed terms 
  to application. But when we do this we can do beta reduction and get  a substitution.
  \item [five]
  \item [six] Define exactly is STLC: for ground types and later for function types. The logical
  relations should leave constants (left-)invariant.
  
  $R_{bool} = \{ (a,b,c)\in B_\bot \mid a=\bot or b=\bot or c=\bot or a=b=c \}$
  
  $R_{int}  = \{ (a,b,c)\in N_\bot \mid a=\bot or b=\bot or c=\bot or a=b=c \}$
  
  Check applying $(succ,succ,succ)$ to the sets.
  
  With $Y$-combinator still no problem (describe as in provious case). And everything else is 
  $\lambda$-calculus.
  
  Look at $(por,por,por)$ and apply it at $(\tt,\bot,\ff), (\bot,\tt,\ff)$ we get
  $(\tt,\tt,\ff)$.
  
  Karl Sieber paper about how to do for a maximum subset of PCF (2 rank types only or something).
  
  
\end{enumerate}

\section{Day5}

\begin{theorem}[``Lemma``]
if $\forall \sigma$: every element of $D_\sigma$ is PCF-definable then the semantics will be 
fully abstract: $M\lesssim_cM' \Rightarrow \sem{M}{} \leq \sem{M'}{}$
\end{theorem}

\begin{proof}
 Induction over type of M/M'.
 
 ground type: $M\lesssim_c M' \Leftrightarrow M\lesssim_a M' \Leftrightarrow$ 
 $(M\Downarrow n \Rightarrow M'\Downarrow n$
 
 $M,M': \sigma \rarr \tau$: $M\lesssim_c M' \Leftrightarrow M\lesssim_a M' \Leftrightarrow$ 
 $\forall N:\sigma: MN\lesssim_a M'N \Leftrightarrow by I.H. \sem{MN}{} \leq \sem{M'N}{}$, i.e.
 $\sem{M}{}(\sem{N}{}) \leq \sem{M}{N}(\sem{M'}{N})$ and by definability 
 $\sem{M}{} \leq \sem{M'}{}$
\end{proof}

The goal now is to make this lemma a useful lemma.

\begin{theorem}[Lemma(Plotkin)]
if $\forall \sigma$: every comapct element of $D_\sigma$ is (PCF+paror)-definable then the 
semantics will be fully abstract: $M\lesssim_cM' \Rightarrow \sem{M}{} \leq \sem{M'}{}$.
\end{theorem}

\begin{definition}
 D is a cpo, $a\in D$ and is called compact if whenever $Vd_n \geq a$ then 
 $d_n \geq a$ for some $n$.
\end{definition}

Example in the power of set al finite sets are compact.

\begin{definition}
 D is \textbf{algebraic} CPO if every element $d\in D$ can be written as $Va_n=d$ with all $a_n$
 compact.
\end{definition}

All subsets of natural numbers are compact because every set is a limit of some finite series of 
subsets.

\begin{definition}
 D is $\omega-$\textbf{algebraic} CPO if every element $d\in D$ can 
 be written as $Va_n=d$ with all $a_n$ compact, and there are only countably many 
 compact elements in $D$.
\end{definition}

Goal: to show that add $D_\sigma$ are $\omega$-algebraic.
\begin{proof}
 Induction over types.
 
 $B_\bot$, $N_\bot$ are $\omega$-algebraic (all chains are finite).
 
 $D_\sigma$ is w-alg. and $D_\tau$ is w-algebriac $\Rightarrow? [D_\sigma \rarr D_\tau]$ is w-alg?
 NO, we need some additional constraints.
\end{proof}

\begin{definition}
 $D$ is a Scott-domain  it is $\omega$-algebraic CPO and for any two elements $x,y\in D$
 there is an  infinum : $x\wedge y$ -- largest lower bound.
\end{definition}

Example of  the case where there is not infinum: let two elements have to uncomparable lower bounds
(5 element: a,b, two lower bound and bottom)
%picture.

\begin{theorem}
 Scott domains form a Cartesion-closed category.
\end{theorem}
\begin{proof}
 $D\times E$, $(x,x')\wedge(y,y') = (x\wedge x', t\wedge y')$.
 
 Let's look at function spaces: $[D\rarr E]$. we have $x$ and $f(x)$ and $c$ below $f(x)$.
 $x$ is a limit of compact
 elements, so $f=V f(d_n)$, because f is continious $ = Vf(d_n) \geq c$. So one of the $d_n$ should 
 have been sent above $c$. By monotonicity all element after $d_n$ go above $c$. Let's make 
 function about it.
 
\[
    d-to-c(x)=\left\{
                \begin{array}{ll}
                  c \text{when} x\geq d\\
                  \bot \text{otherwise}
                \end{array}
              \right.
  \]

  We introduced step functions.
  
  $K[D\rarr E] reversly \in d-to-c$.
  
  So the function is supremum of step functions but we cannot arrange step functions to the chain,
  and to do this we need ''meet`` operation.
\end{proof}

\begin{theorem}
Goal: $D_\sigma$ are Scott-domain.  (upgrade of previous failed goal)
\end{theorem}

\begin{proof}
 Induction over types.
 
 $B_\bot$, $N_\bot$ are $\omega$-algebraic (all chains are finite).
 
 $D_\sigma$ is w-alg. and $D_\tau$ is w-algebriac $\Rightarrow? [D_\sigma \rarr D_\tau]$ is w-alg?
 
 $\sem{M}{}\leq\sem{M'}{} \Leftrightarrow$ $\forall a . \sem{M}{}(a)\leq\sem{M'}{}(a)$
 $\Leftrightarrow$ $\forall a \in K(D_\sigma). \sem{M}{}(a)\leq\sem{M'}{}(a)$. So, it's enough to 
 test it on compact.
 
 % я не совсем понял часть ли это доказателства но он начал жоказывать новую лемму.
\end{proof}

\begin{theorem}[Lemma]
 $f,g: D\rarr E$, $D$ and $E$ are alg. Then $f\leq g \Leftrightarrow\forall a\in K(D)$:
 $d(a)\leq g(a)$.
\end{theorem}

\begin{proof}
 $x\in D$. want $d(x) \leq g(x)$, $x=Va_n$. Let c compact be below $f(x)$
 
 $g(x) = f(Va_n) = Vf(a_n) \geq Vf(a_n) = f(Va_n) = f(x)$
\end{proof}

Question: why Scott-condition was needed?

Exercise: $D$ is Scott-domain. $A\subseteq D$ boudded by $x\in D$ ($A\leq x)$. Then
''joins`` $\wedge A$ exists.

We already know that Scott-model is not fully abstract for PCF (because parallel or is not 
definable).

\begin{theorem}[Milner, 77]
 There exists a fully abstract model for PCF which consists of Scott-domains
\end{theorem}

He pick term model factored by $\alpha\beta\eta$-equivalence.
 
Full abstraction problem. Nobody did it strightforwardly because it is undecideable to detect all
uncomutable elements
 
\begin{theorem}[Loader'01]
There is no effective presentation of Milner's model.
\end{theorem}

Game semantics was built because of that problem (by three independent groups). And folks
showed that they cn construct fully abstract semantics.
\begin{theorem}
Game model does not consist of CPOs.
\end{theorem}
It doesn't violate Loader's result.


Now we discuss an untyped \lambda-calculus.

It took about 40 years to obtain first model for the untyped \lambda-calculus.

Grammar: $M ::= x \mid MM \mid \lambda x . m$

$\sem{\cdot}{}: \Lambda \rarr D$ -- we give semantics in the one set, because everthing have the
same (still no) type.

$\sem{x}{} = \rho(x)$

$\sem{MN}{\rho} = \sem{M}{\rho} ( \sem{N}{\rho})$. if we look to it abstractly we will go to 
combinatory algebra. Another way to look at it as functions. We need an operation whih converts
$D$ to $[D\rarr D]$, and $\sem{MN}{\rho} = \sem{M}{\rho} ( \sem{N}{\rho}) = \psi (\sem{M}{\rho})( \sem{N}{\rho})$

$\sem{\lambda x. M}{\rho} = \Psi(a \mapsto \sem{M}{\rho[x\mapsto a]}).$

% Что такое Фи я не записал

\begin{theorem}[Substitution Lemma]
 holds verbatim.
\end{theorem}

\begin{theorem}[Correctness]
 Equivalence relations hold, congruence rules holds, $\alpha$ holds.
 $\beta$ holds if $\psi \circ \phi = id_{D\rarr D}$. 
 $\eta$ hiolds if $\phi \circ \psi = id_D$
\end{theorem}

\begin{proof}
 $\beta$: $\sem{(\lambda x . M)N}{\rho} = \psi (\sem{\lambda x . M}{\rho})(\sem{N}{\rho})$
 $\psi (\phi (a \mapsto \sem{M}{\rho[x \mapsto a]))(\sem{N}{\rho}$
 
 by ass $\sem{M}{\rho[x\mapsto \sem{N}{\rho}]}$
\end{proof}

the problem. $\psi$ and $\phi$ need to be bijections, i.e. D nad $[D\rarr D]$ are in bijections.
But this can never be happen , only in one element set. Because of cardinality issues.

$\mid D\rarr D\mid  = \mid w^D\mid > \mid D \mid$

but we cn't use single-element sets because very functions should have fixpoint because

$Y=\lambda f . (\lambda x. f(x x)) (\lambda x. f(x x))$ and $YM=M(YM)$.

The next idea of Scott was to construct 2, $[2\rarr2]$, $[2\rarr2] \rarr [2\rarr2]$, etc and get
a limit.

To get a limit we need somehow say that one set is larger than another.

$2 \leftrightharpoons [2\rarr 2]$ from right it is projection, and from the left is embedding.

$e(d) = \lambda x . d$ and $p(f) = f(\bot)$.

There is a good property about this two functions: $p(e(d)=d$ then $p \cdot e = id_D$.
$e(p(f)) \leq f$, $e\cdot p \leq id_{(D\rarr D)}$. \textit{Embedding-projection pair.}

For $ [2\rarr 2] \leftrightharpoons [[2\rarr 2]\rarr  [2\rarr 2]]$ we will not do exactly the same.
Will use $p_1$ and $e_1$ as projectio/embedding functions.

we will try to get a link from $(e,p)$ to $e_1,p_1)$.
% картинка которую не зарисовывал.

$e_1=\lambda f . e\circ f\circ p$ and $p_1 = \lambda f. p\circ f\circ e$

$p_1\circ e_1(f) = pefpe = f$ and $e1\circ p_1(f) = epfep \leq f$.

% каринка с $D_i$ and F^nD_0

$D_\inf$ = {$(a_n) \mid \forall n: a_n = p(a_{n+1})$} 

And to get from $D_\inf$ to $F^2D$ we just need to take 2nd element of sequence.

After applying functor $F$ we will get $F$ everywhere and also $[D_\inf\rarr D\inf]$, object 
such that there are some links and by categorial nonse we will have link between $D\inf$ and
$[D_\inf\rarr D_\inf]$. It will not be $e,p$ pair, it will be pair of isomorphisms.

% recommended chapter from book by daniel abramsky by the lecturer. Chapter 4 or 6.

Here our models depend on starting $D$ but in PCF there is  canonical model.

Recursive domain equations.

Domain of lists: $L = 1+D*L$ has canonical solution in set and domain theory. Because there is
no contrvariant argument as or functions. we can describ all recursive types like this.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{prooftree}
 \AxiomC{$ $}
 \AxiomC{$ $}
 \BinaryInfC{$ $}
\end{prooftree}


\end{document}