i.数学基础-lecture notes on the lambda calculus

1. functions as graphs
2. functions as formulas

1. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions.

1. Untyped lambdacalculus.
2. Simply-typed lambda calculus.
3. Polymorphically typed lambda calculus.

1. Many real-world programming languages can be regarded as extensions of the lambda calculus.

1. The connection between lambda calculus and constructive logics is via the “proofs-as-programs” paradigm.

1. lambda terms: variables, applications, and lambda abstractions
2. Backus-Naur Form:$$M,N ::= xmid (MN)mid (lambda x.M)$$

1. If $x, y$ are variables, and $M$ is a term, we write $M{y/x}$ for the result of renaming $x$ as $y$ in $M$.
2. We define $alphatextit{-equivalence}$ to be the smallest congruence relation $=_{alpha}$ on lambda terms, such that for all terms $M$ and all variables $y$ that do not occur in $M$,$$lambda x.M =_{alpha} lambda y.(M{y/x}),ynotin FV(M)$$

1. We will write $M[N/x]$ for the result of replacing $x$ by $N$ in $M$.
2. We should only replace free variables.

1. We will often use the ordinary equality symbol $M = N$ to denote $alphatextit{-equivalence}$.
2. The process of evaluating lambda terms by “plugging arguments into functions” is called $betatextit{-reduction}$.$$(lambda x.M)Nrightarrow_{beta}M[N/x]$$
3. A lambda term without any β-redexes is said to be in $betatextit{-normal form}$.

1. $mathbf{Definition.}$ We write $Mtwoheadrightarrow_{beta} M’$ if $M$ reduces to $M’$ in zero or more steps. Formally, $twoheadrightarrow_{beta}$ is defined to be the reflexive transitive closure of $rightarrow_{beta}$.
2. $mathbf{Definition.}$ We write $M =_{beta} M’$ if $M$ can be transformed into $M’$ by zero or more reduction steps and/or inverse reduction steps.Formally, $=_{beta}$ is defined to be the reflexive symmetric transitive closure of $rightarrow_{beta}$.
3. 好好看一下Closure

1. $$begin{split}&T=lambda xy.xcr &F=lambda xy.yend{split}$$
2. 如果逻辑运算符“and”定义为：$lambda ab.abF$，则$$begin{split}&mathbf{and} TTtwoheadrightarrow_{beta}Tcr &mathbf{and} TFtwoheadrightarrow_{beta}Fcr &mathbf{and} FTtwoheadrightarrow_{beta}Fcr &mathbf{and} FFtwoheadrightarrow_{beta}Fcrend{split}$$

1. If $F$ and $N$ are lambda terms, we say that $N$ is a fixed point of $F$ if $FN =_{beta} N$
2. $mathbf{Theorem 3.1}textit{ In the untyped lambda calculus, every term F has a fixed point.}$
3. $mathbf{Proof}$. Let $A = lambda xy.y(xxy)$, and define $theta = AA$. Now suppose $F$ is any lambda term, and let $N = theta F$ . We claim that $N$ is a fixed point of $F$ . This is shown by the following calculation:$$begin{split}N&=theta Fcr
   &=AAFcr
   &=(lambda xy.y(xxy))AFcr
   &rightarrow_{beta}F(AAF)cr
   &=F(theta F)cr
   &=FNend{split}$$
4. The term $theta$ used in the proof is called Turing’s fixed point combinator.

1. $etatextit{-reduction}$:$$lambda x.Mxrightarrow_{eta} M, textit{where} xnotin FV(M)$$
2. Single-step $betaeta$-reduction $rightarrow_{betaeta}$ is defined as the union of the single-step $beta$- and $eta$-reductions

1. $mathbf{Theorem 4.2}$ (Church and Rosser, 1936):
   Suppose $M$, $N$, and $P$ are lambda terms such that $M twoheadrightarrow N$ and $M twoheadrightarrow P$. Then there exists a lambda term $Z$ such that $N twoheadrightarrow Z$ and $P twoheadrightarrow Z$.

1. 很有意思，帮助理解，但一些图太难画了。

1. We begin by defining a new relation $M rhd M’$ on terms, called $textit{parallel one-step reduction}$. We define $rhd$ to be the smallest relation satisfying:$$begin{split}&frac{}{xrhd x}cr
   &frac{Prhd P’,Nrhd N’}{PNrhd P’N’}cr
   &frac{Nrhd N’}{lambda x.Nrhdlambda x.N’}cr
   &frac{Qrhd Q’,Nrhd N’}{(lambda x.Q)Nrhd Q’[N’/x]}cr
   &frac{Prhd P’(xnotin FV(P))}{lambda x.Pxrhd P’}end{split}$$
2. $mathbf{Lemma 4.6}$:
   • (a) For all $M$, $M’$, if $Mrightarrow_{betaeta} M’$ then $M rhd M’$.
   • (b) For all $M$, $M’$, if $Mrhd M’$ then $M twoheadrightarrow_{betaeta} M’$.
   • (c) $twoheadrightarrow_{betaeta}$ is the reflexive transitive closure of $rhd$.
3. $mathbf{Lemma 4.7}$ (Substitution).If $M rhd M’$ and $U rhd U’$, then $M[U/y] rhd M’[U’/y]$.
4. $mathbf{Lemma 4.8}$ (Maximal parallel one-step reductions). Whenever $M rhd M’$, then $M’ rhd M^*$.
5. $mathbf{Lemma 4.9}$ (Diamond property for $rhd$). If $M rhd N$ and $M rhd P$ , then there exists $Z$
   such that $N rhd Z$ and $P rhd Z$.
6. $textit{Proof of Theorem 4.2}$: Since $rhd$ satisfies the diamond property, and its reflexive transitive closure $twoheadrightarrow_{betaeta}$ also satisfies the diamond property,and the diamond property for $twoheadrightarrow_{betaeta}$ is just the Church-Rosser property for $rightarrow_{betaeta}$.

5.1 Applicative structures

1. $mathbf{Definition.}$ Let $(A, ·)$ be an applicative structure. the set of polynomials is given by the following grammar:
   $$t,s ::= x|a|ts$$

5.2 Combinatory completeness

1. $mathbf{Definition}$ (Combinatory completeness). An applicative structure $(A, ·)$ is combinatorially complete if for every polynomial $t(x_1 , . . . , x_n )$ of $n geqslant 0$ variables, there exists some element $a in A$ such that
   $$ax_1 …x_n = t(x_1,…,x_n)$$
   holds in A.
2. $mathbf{Theorem 5.1.}$ An applicative structure $(A, ·)$ is $textit{combinatorially complete}$ if and only if there exist two elements $s, k in A$, such that the following equations are satisfied for all $x, y, z in A$:$$begin{split}&sxyz = (xz)(yz),cr &kxy = xend{split}$$
3. 已经看得云里雾里了，不明白定义和定理的用意。

5.3 Combinatory algebras

1. We usually use the Greek letter $iota$ to denote a basic type. The set of simple types is given by the following BNF:
   $$textit{Simple types}: A,B::=iotamid Ato B mid A×B mid 1$$

1. whether it is possible to find a closed term of the given type.
2. This connection between simply-typed lambda calculus and propositional logic is known as the “Curry-Howard isomorphism”.
3. The main difference between intuitionistic and classical logic is that the former misses the principles of “proof by contradiction” and “excluded middle”.
4. Intuitionistic logic is also known as constructive logic. The disadvantage of constructive logic is that it is generally more difficult to prove things. The advantage is that once one has a proof, the proof can be transformed into an algorithm.