Lambda calculus

Lambda Calculus Syntax

content/lambda-calculus/syntax/syntax.tex

% Part: lambda-calculus% Chapter: syntax\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{lam}{syn}{Syntax}\olimport{terms}\olimport{unique-readability}\olimport{abbreviated-syntax}\olimport{free-variables}\olimport{substitution}\olimport{alpha}\olimport{de-bruijn}\olimport{term-revisited}\olimport{beta}\olimport{eta}\OLEndChapterHook\end{document}

content/lambda-calculus/syntax/terms.tex

% Part: lambda-calculus% Chapter: syntax% Section: terms\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{trm}\olsection{Terms}The terms of the lambda calculus are built up inductively from aninfinite supply of variables $\Obj{v_0}$, $\Obj{v_1}$, \dots, thesymbol~``$\lambd$'', and parentheses. We will use $x$, $y$, $z$, \dots{}to designate variables, and $M$, $N$, $P$, \dots{} to desginate terms.\begin{defn}[Terms] \ollabel{defn:term}The set of \emph{terms} of the lambda calculus is defined inductively by:\begin{enumerate}  \item \ollabel{defn:term-var} If $x$ is a variable, then $x$ is a    term.  \item \ollabel{defn:term-abs} If $x$ is a variable and $M$ is a    term, then $(\lambd[x][M])$ is a term.  \item \ollabel{defn:term-app} If both $M$ and $N$ are terms, then    $(MN)$ is a term.\end{enumerate}\end{defn}If a term $(\lambd[x][M])$ is formed according to\olref{defn:term-abs} we say it is the result of an\emph{abstraction}, and the $x$ in $\lambd[x]$ is called a\emph{!!{parameter}}.  A term $(MN)$ formed according to\olref{defn:term-app} is the result of an \emph{application}.The terms defined above are fully parenthesized. This can get rathercumbersome, as the term$(\lambd[x][((\lambd[x][x])(\lambd[x][(xx)]))])$ demnostrates. We willintroduce conventions for avoiding parentheses.  However, the officialdefinition makes it easy to determine how a term is constructedaccording to \olref{defn:term}. For example, the last step of formingthe term $(\lambd[x][((\lambd[x][x])(\lambd[x][(xx)]))])$ must beabstraction where the !!{parameter} is~$x$. It results by abstractionfrom the term $((\lambd[x][x])(\lambd[x][(xx)]))$, which is anapplication of two terms. Each of these two terms is the result of anabstraction, and so on.\begin{prob}Describe the formation of $(\lambd[g][(\lambd[x][(g (x x))])  (\lambd[x][(g (x x))])])$.\end{prob}\end{document}

content/lambda-calculus/syntax/unique-readability.tex

% Part: lambda-calculus% Chapter: introduction% Section: unique-readability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{unq}\olsection{Unique Readability}We may wonder if for each term there is a unique way of forming it,and there is.  For each lambda term there is only one way to constructand interpret it.  In the following discussion, a \emph{formation} isthe procedure of constructing a term using the formation rules (one orseveral times) of \olref[trm]{defn:term}.\begin{lem}\ollabel{lem:term-start}A term starts with either a variable or a parenthesis.\end{lem}\begin{proof}Something counts as a term only if it is constructed according to\olref[trm]{defn:term}. If it is the result of\olref[trm]{defn:term-var}, it must be a variable. If it is the resultof \olref[trm]{defn:term-abs} or \olref[trm]{defn:term-app}, it startswith a parenthesis.\end{proof}\begin{lem}\ollabel{lem:app-start}The result of an application starts with either two parentheses or aparenthesis and a variable.\end{lem}\begin{proof}If $M$ is the result of an application, it is of the form $(PQ)$, soit begins with a parenthesis. Since $P$ is a term, by\olref{lem:term-start}, it begins either with a parenthesis or avariable.\end{proof}\begin{lem}\ollabel{lem:initial}No proper initial part of a term is itself a term.\end{lem}\begin{prob}Prove \olref[lam][syn][unq]{lem:initial} by induction on the lengthof terms.\end{prob}\begin{prop}[Unique Readability] \ollabel{prop:unq}There is a unique formation for each term. In other words, if a term$M$ is formed by a formation, then it is the only formation that canform this term.\end{prop}\begin{proof}  We prove this by induction on the formation of terms.   \begin{enumerate}    \item $M$ is of the form      $x$, where $x$ is some variable. Since the results of abstractions and applications always start with parentheses, they cannot have been used to      construct $M$; Thus, the formation of $M$ must be a single step      of \olref[trm]{defn:term}\olref[trm]{defn:term-var}.    \item $M$ is of the form $(\lambd[x][N])$, where $x$ is some      variable and $N$ is a term. It could not have been constructed      according to \olref[trm]{defn:term}\olref[trm]{defn:term-var},      because it is not a single variable.  It is not the result of an      application, by \olref{lem:app-start}. Thus $M$ can only be the      result of an abstraction on~$N$.  By inductive hypothesis we      know that formation of $N$ is itself unique.    \item $M$ is of the form $(PQ)$, where $P$ and $Q$ are terms.      Since it starts with a parentheses, it cannot also be      constructed by      \olref[trm]{defn:term}\olref[trm]{defn:term-var}.  By      \olref{lem:term-start}, $P$ cannot begin with $\lambd$, so      $(PQ)$ cannot be the result of an abstraction.  Now suppose      there were another way of constructing $M$ by application, e.g.,      it is also of the form $(P'Q')$. Then $P$ is a proper initial      segment of $P'$ (or vice versa), and this is impossible by      \olref{lem:initial}. So $P$ and $Q$ are uniquely      determined, and by inductive hypothesis we know that formations      of $P$ and $Q$ is unique.  \end{enumerate}\end{proof}A more readable paraphrase of the above proposition is as follows:\begin{prop}  A term $M$ can only be one of the following forms:  \begin{enumerate}    \item $x$, where $x$ is a variable uniquely determined by $M$.    \item $(\lambd[x][N])$, where $x$ is a variable and $N$ is      another term, both of which is uniquely determined by $M$.    \item $(PQ)$, where $P$ and $Q$ are two terms uniquely      determined by $M$.  \end{enumerate}\end{prop}\end{document}

content/lambda-calculus/syntax/abbreviated-syntax.tex

% Part: lambda-calculus% Chapter: syntax% Section: abbreviated-syntax\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{abb}\olsection{Abbreviated Syntax}Terms as defined in \olref[trm]{defn:term} are sometimes cumbersome towrite, so it is useful to introduce a more concise syntax. We must ofcourse be careful to make sure that the terms in the concise notationalso are uniquely readable.  One widely used version called\emph{abbreviated terms} is as follows.\begin{enumerate}\item When parentheses are left out, application takes place from left  to right. For example, if $M$, $N$, $P$, and~$Q$ are terms, then  $MNPQ$ abbreviates $(((MN)P)Q)$.\item Again, when parentheses are left out, lambda abstraction is  given the widest scope possible. From example, $\lambd[x][MNP]$ is  read as $(\lambd[x][MNP])$.\item A lambda can be used to abstract multiple variables. For  example, $\lambd[xyz][M]$ is short for  $\lambd[x][\lambd[y][\lambd[z][M]]]$.\end{enumerate}For example,\[\lambd[xy][xxyx \lambd[z][xz]]\]abbreviates\[(\lambd[x][(\lambd[y][((((xx)y)x)(\lambd[z][(xz)]))])]).\]\begin{prob}Expand the abbreviated term $\lambd[g][(\lambd[x][g (x x)])  \lambd[x][g (x x)]]$.\end{prob}\end{document}

content/lambda-calculus/syntax/free-variables.tex

% Part: lambda-calculus% Chapter: introduction% Section: free-variables\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{fv}\olsection{Free Variables}Lambda calculus is about functions, and lambda abstraction is howfunctions arise. Intuitively, $\lambd[x][M]$ is the function withvalues given by~$M$ when the argument to the function is assignedto~$x$. But not every occurrence of~$x$ in~$M$ is relevant: if $M$contains another abstract $\lambd[x][N]$ then the occurrences of $x$in~$N$ are relevant to $\lambd[x][N]$ but not to $\lambd[x][M]$.  So,a lambda abstract $\lambd[x]$ inside $\lambd[x][M]$ \emph{binds} thoseoccurrences of $x$ in~$M$ that are not already bound by another lambdaabstract---the \emph{free} occurrences of~$x$ in~$M$.\begin{defn}[Scope]If $\lambd[x][M]$ occurs inside a term~$N$, then the correspondingoccurrence of~$N$ is the \emph{scope} of the~$\lambd[x]$.\end{defn}\begin{defn}[Free and bound occurrence]  An occurrence of variable $x$ in a term~$M$ is \emph{free} if it is  not in the scope of a $\lambd[x]$, and \emph{bound} otherwise. An  occurrence of a variable~$x$ in $\lambd[x][M]$ is bound by the initial  $\lambd[x]$ iff the occurrence of $x$ in~$M$ is free.\end{defn}\begin{ex}  In $\lambd[x][x y]$, both $x$ and $y$ are in the scope of $\lambd[x]$,  so $x$ is bound by $\lambd[x]$. Since $y$ is not in the scope of  any $\lambd[y]$, it is free.  In $\lambd[x][x x]$, both occurrences  of $x$ are bound by~$\lambd[x]$, since both are free in $xx$.  In  $((\lambd[x][xx])x)$, the last occurrence of~$x$ is free, since it  is not in the scope of a $\lambd[x]$. In  $\lambd[x][(\lambd[x][x])x]$, the scope of the first $\lambd[x]$ is  $(\lambd[x][x])x$ and the scope of the second $\lambd[x]$ is the  second-to-last occurrence of~$x$. In $(\lambd[x][x])x$, the last  occurrence of $x$ is free, and the second-to-last is bound.  Thus,  the second-to-last occurrence of $x$ in $\lambd[x][(\lambd[x][x])x]$  is bound by the second $\lambd[x]$, and the last occurrence by the  first $\lambd[x]$.\end{ex}For a term $P$, we can check all variable occurrences in it and get aset of free variables. This set is denoted by $\FV{P}$ with a naturaldefinition as follows:\begin{defn}[Free variables of a term] \ollabel{def:fv}  The set of \emph{free variables} of a term is defined inductively by:  \begin{enumerate}    \item $\FV{x} = \{x\}$ \ollabel{def:fv1}     \item $\FV{\lambd[x][N]} = \FV{N} \setminus \{x\}$    \ollabel{def:fv2}    \item $\FV{PQ} = \FV{P} \cup \FV{Q}$ \ollabel{def:fv3}  \end{enumerate}\end{defn}\begin{prob}  \begin{enumerate}  \item Identify the scopes of $\lambd[g]$ and the two $\lambd[x]$ in    this term: $\lambd[g][(\lambd[x][g (x x)]) \lambd[x][g (x x)]]$.  \item In $\lambd[g][(\lambd[x][g (x x)]) \lambd[x][g (x x)]]$, are    all occurrences of variables bound? By which abstractions are they    bound respectively?    \item Give $\FV{\lambd[x][(\lambd[y][(\lambd[z][x y]) z]) y]}$  \end{enumerate}\end{prob}\begin{explain}A free variable is like a reference to the outside world (the\emph{environment}), and a term containing free variables can be seenas a partially specified term, since its behaviour depends on how weset up the environment. For example, in the term $\lambd[x][f x]$, whichaccepts an argument~$x$ and returns $f$ of that argument, thevariable~$f$ is free. This value of the term is dependent on theenvironment it is in, in particular the value of $f$ in thatenvironment.If we apply abstraction to this term, we get $\lambd[f][\lambd[x][f    x]]$. This term is no longer dependent on the environment variable$f$, because it now designates a function that accepts two argumentsand returns the result of applying the first to the second. Changing$f$ in the environment won't have any effect on the behavior of thisterm, as the term will only use whatever is passed as an argument, andnot the value of $f$ in the environment.\end{explain}\begin{defn}[Closed term, combinator]  A term with no free variables is called a \emph{closed term}, or a  \emph{combinator}.\end{defn}\begin{lem}\ollabel{lem:fv}  \begin{enumerate}    \item \ollabel{lem:fv-abs} If $y \neq x$, then $y \in      \FV{\lambd[x][N]}$ iff $y \in \FV{N}$.    \item \ollabel{lem:fv-app} $y \in \FV{PQ}$ iff $y \in \FV{P}$ or $y      \in \FV{Q}$.    \end{enumerate}\end{lem}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[lam][syn][fv]{lem:fv}.\end{prob}\end{document}

content/lambda-calculus/syntax/substitution.tex

% Part: lambda-calculus% Chapter: syntax% Section: substitution\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{sub}\olsection{Substitution}\begin{explain}Free variables are references to environment variables, thus it makessense to actually use a specific value in the place of a freevariable. For example, we may want to replace $f$ in $\lambd[x][f x]$with a specific term, like the identity function $\lambd[y][y]$. Thisresults in $\lambd[x][(\lambd[y][y]) x]$. The process of replacingfree variables with lambda terms is called substitution.\end{explain}\begin{defn}[Substitution] \ollabel{defn:substitution}  The \emph{substitution} of a term $N$ for a variable $x$ in a term  $M$, $\Subst{M}{N}{x}$, is defined inductively by:  \begin{enumerate}    \item $\Subst{x}{N}{x} = N$. \ollabel{defn:substitution-1}     \item $\Subst{y}{N}{x}  = y$ if $x \neq y$. \ollabel{defn:substitution-2}     \item $\Subst{PQ}{N}{x}  = (\Subst{P}{N}{x}) (\Subst{Q}{N}{x})$.      \ollabel{def:substitution-3}    \item $\Subst{(\lambd[y][P])}{N}{x} = \lambd[y][\Subst{P}{N}{x}]$,      if $x \neq y$ and $y \notin \FV{N}$, otherwise undefined.      \ollabel{defn:substitution-4}  \end{enumerate}\end{defn}\begin{explain}In \olref{defn:substitution}\olref{defn:substitution-4}, we require $x\neq y$ because we don't want to replace \emph{bound} occurrences ofthe variable~$x$ in~$M$ by~$N$.  For example, if we compute thesubstitution $\Subst{\lambd[x][x]}{y}{x}$, the result should not be$\lambd[x][y]$ but simply $\lambd[x][x]$.When substituting $N$ for~$x$ in $\lambd[y][P]$, we also require that$y \notin \FV{N}$.  For example, we cannot substitute $y$ for $x$ in$\lambd[y][x]$, i.e., $\Subst{\lambd[y][x]}{y}{x}$, because it wouldresult in $\lambd[y][y]$, a term that stands for the function thataccepts an argument and returns it directly. But the term$\lambd[y][x]$ stands for a function that always returns the term~$x$(or whatever $x$ refers to). So the result we actually want is afunction that accepts an argument, drop it, and returns theenvironment variable~$y$. To do this properly, we would first have to``rename'' the bound variable~$y$.\end{explain}\begin{prob}  What is the result of the following substitutions?  \begin{enumerate}  \item $\Subst{\lambd[y][x(\lambd[w][vwx])]}{(uv)}{x}$  \item $\Subst{\lambd[y][x(\lambd[x][x])]}{(\lambd[y][xy])}{x}$  \item $\Subst{y(\lambd[v][xv])}{(\lambd[y][vy])}{x}$  \end{enumerate}\end{prob}\begin{thm} \ollabel{thm:notinfv}  If $x \notin \FV{M}$, then $\FV{\Subst{M}{N}{x}} = \FV{M}$, if  the left-hand side is defined.\end{thm}\begin{proof}  By induction on the formation of $M$.  \begin{enumerate}  \item $M$ is a variable: exercise.  \item $M$ is of the form $(PQ)$: exercise.  \item $M$ is of the form $\lambd[y][P]$, and since    $\Subst{\lambd[y][P]}{N}{x}$ is defined, it has to be    $\lambd[y][\Subst{P}{N}{x}]$. Then $\Subst{P}{N}{x}$ has to be    defined; also, $x \neq y$ and $x \notin \FV{Q}$. Then:    \begin{multline*}      \FV{\Subst{\lambd[y][P]}{N}{x}} = \\    \begin{aligned}      & = \FV{\lambd[y][\Subst{P}{N}{x}]} &&      \text{by \olref{defn:substitution-4}}\\      & = \FV{\Subst{P}{N}{x}} \setminus \{y\} &&      \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}}\\      & = \FV{P} \setminus \{y\} && \text{by inductive hypothesis} \\      & = \FV{\lambd[y][P]} && \text{by \olref[fv]{def:fv}\olref[fv]{def:fv2}}    \end{aligned}    \end{multline*}  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][sub]{thm:notinfv}.\end{prob}\begin{thm} \ollabel{thm:infv}  If $x \in \FV{M})$, then $\FV{\Subst{M}{N}{x}} = (\FV{M} \setminus  \{x\}) \cup \FV{N}$, provided the left hand is defined.\end{thm}\begin{proof}  By induction on the formation of $M$.  \begin{enumerate}  \item $M$ is a variable: exercise.  \item $M$ is of the form $PQ$: Since    $\Subst{(PQ)}{N}{y}$ is defined, it has to be    $(\Subst{P}{N}{x})(\Subst{Q}{N}{x})$ with both substitution    defined. Also, since $x \in \FV{PQ}$, either $x \in \FV{P}$ or    $x \in \FV{Q}$ or both. The rest is left as an exercise.  \item $M$ is of the form $\lambd[y][P]$. Since    $\Subst{\lambd[y][P]}{N}{x}$ is defined, it has to be    $\lambd[y][\Subst{P}{N}{x}]$, with $\Subst{P}{N}{x}$    defined, $x \neq y$ and $y \notin \FV{N}$; also, since $y \in    \FV{\lambd[x][P]}$, we have $y \in \FV{P}$ too. Now:    \begin{multline*}      \FV{\Subst{(\lambd[y][P])}{N}{x}} = \\      \begin{aligned}      & = \FV{\lambd[y][\Subst{P}{N}{x}]} \\      & = \FV{\Subst{P}{N}{x}} \setminus \{y\} \\      & = ((\FV{P} \setminus \{y\}) \cup (\FV{N} \setminus \{x\})       && \text{by inductive hypothesis} \\      & = (\FV{P} \setminus \{x, y\}) \cup \FV{N}       && x \notin \FV{N} \\      & = (\FV{\lambd[y][P]} \setminus \{x\}) \cup \FV{N}      \end{aligned}      \end{multline*}  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][sub]{thm:infv}.\end{prob}\begin{thm}\ollabel{thm:clr}  $x \notin \FV{\Subst{M}{N}{x}}$, if the right-hand side is  defined and $x \notin \FV{N}$.\end{thm}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[lam][syn][sub]{thm:clr}.\end{prob}\begin{thm}\ollabel{thm:inv}  If $\Subst{M}{y}{x}$ is defined and $y \notin \FV{M}$, then  $\Subst{\Subst{M}{y}{x}}{x}{y} = M$.\end{thm}\begin{proof}  By induction on the formation of $M$.  \begin{enumerate}  \item $M$ is a variable $z$: Exercise.  \item $M$ is of the form $(PQ)$. Then:    \begin{align*}      \Subst{\Subst{(PQ)}{y}{x}}{x}{y}      &=\Subst{((\Subst{P}{y}{x})(\Subst{Q}{y}{x}))}{x}{y} \\      &= (\Subst{\Subst{P}{y}{x}}{x}{y})(\Subst{\Subst{Q}{y}{x}}{x}{y}) \\      &= (PQ) \text{ by inductive hypothesis}    \end{align*}  \item $M$ is of the form $\lambd[z][N]$. Because    $\Subst{\lambd[z][N]}{y}{x}$ is defined, we know    that $z \neq y$. So:    \begin{align*}      \Subst{\Subst{(\lambd[z][N])}{y}{x}}{x}{y}\\      & = \Subst{(\lambd[z][\Subst{N}{y}{x}])}{x}{y} \\      & = \lambd[z][\Subst{\Subst{N}{y}{x}}{x}{y}] \\      &= \lambd[z][N] \text{ by inductive hypothesis}     \end{align*}  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][sub]{thm:inv}.\end{prob}\end{document}

content/lambda-calculus/syntax/alpha.tex

% Part: lambda-calculus% Chapter: syntax% Section: alpha\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{alp}\olsection{$\alpha$-Conversion}What is the relation between $\lambd[x][x]$ and $\lambd[y][y]$? Theyboth represent the identity function. They are, of course,syntactically different terms. They differ only in the name of thebound variable, and one is the result of ``renaming'' the boundvariable in the other. This is called \emph{$\alpha$-conversion}.\begin{defn}[Change of bound variable, $\aconvone$]  If a term $M$ contains an occurrence of $\lambd[x][N]$, $y \notin  \FV{N}$, and $\Subst{N}{y}{x}$ is defined, then replacing this occurrence  by   \begin{equation*}    \lambd[y][\Subst{N}{y}{x}]  \end{equation*}  resulting in $M'$ is called a \emph{change of bound variable}, written  as $M \redone[\alpha] M'$.\end{defn}\begin{defn}[Compatibility of relation]  A relation $R$ on terms is said to be \emph{compatible}  if it satisfies following conditions:  \begin{enumerate}  \item If $R N N'$ then $R \lambd[x][N] \lambd[x][N']$  \item If $R P P'$ then $R (PQ) (P'Q)$  \item If $R Q Q'$ then $R (PQ) (PQ')$  \end{enumerate}\end{defn}Thus let's rephrase the definition:\begin{defn}[Change of bound variable, $\aconvone$]  \emph{Change of bound variable} ($\redone[\alpha]$) is   the smallest compatible relation on terms satisfying following  condition:  \begin{align*}    &\lambd[x][N] \redone[\alpha] \lambd[y][\Subst{N}{y}{x}] && \text{if      $x \neq y$, $y \notin \FV{N}$} \\    & &&\text{and $\Subst{N}{y}{x}$ is defined}  \end{align*}\end{defn}``Smallest'' here means the relation contains only pairs that are required bycompatibility and the additional condition, and nothing else. Thusthis relation can also be defined as follows:\begin{defn}[Change of bound variable, $\aconvone$] \ollabel{defn:aconvone}  \emph{Change of bound variable} ($\aconvone$) is inductively  defined as follows:  \begin{enumerate}  \item If $N \aconvone N'$ then $\lambd[x][N] \aconvone    \lambd[x][N']$ \ollabel{defn:aconvone1}  \item If $P \aconvone P'$ then $(PQ) \aconvone (P'Q)$ \ollabel{defn:aconvone2}  \item If $Q \aconvone Q'$ then $(PQ) \aconvone (PQ')$ \ollabel{defn:aconvone3}  \item If $x \neq y$, $y \notin \FV{N}$ and $\Subst{N}{y}{x}$ is defined, then    $\lambd[x][N] \redone[\alpha] \lambd[y][\Subst{N}{y}{x}]$.    \ollabel{defn:aconvone4}  \end{enumerate}\end{defn}The definitions are equivalent, but we leave the proof as anexercise. From now on we will use the inductive definition.\begin{defn}[$\alpha$-conversion, $\aconv$]  \emph{$\alpha$-conversion} ($\aconv$) is the smallest reflexitive  and transitive relation on terms containing $\aconvone$.\end{defn}As above, ``smallest'' means the relation only contains pairs requiredby transitivity, and $\aconvone$, which leads to the followingequivalent definition:\begin{defn}[$\alpha$-conversion, $\aconv$] \ollabel{defn:aconv}  \emph{$\alpha$-conversion} ($\aconv$) is inductively defined as follows:  \begin{enumerate}  \item If $P \aconv Q$ and $Q \aconv R$, then $P \aconv R$.    \ollabel{defn:aconv1}  \item If $P \aconvone Q$, then $P \aconv Q$. \ollabel{defn:aconv2}  \item $P \aconv P$. \ollabel{defn:aconv3}  \end{enumerate}\end{defn}\begin{ex}  $\lambd[x][f x]$ $\alpha$-converts to $\lambd[y][f  y]$, and conversely. Informally  speaking, they are both functions that accept an argument and  return $f$ of that argument, refering to the environment variable~$f$.  $\lambd[x][f x]$ does not $\alpha$-convert to $\lambd[x][g    x]$. Informally speaking, they refer to the environment variables  $f$ and~$g$ respectively, and this makes them different functions: they  behave differently in environments where $f$ and $g$ are different.\end{ex}\begin{prob}  Are the following pairs of terms $\alpha$-convertible?  \begin{enumerate}  \item $\lambd[x][\lambd[y][x]]$ and $\lambd[y][\lambd[x][y]]$  \item $\lambd[x][\lambd[y][x]]$ and $\lambd[c][\lambd[b][a]]$  \item $\lambd[x][\lambd[y][x]]$ and $\lambd[c][\lambd[b][a]]$  \end{enumerate}\end{prob}\begin{lem}\ollabel{lem:fv-one}  If $P \aconvone Q$ then $\FV{P} = \FV{Q}$.\end{lem}\begin{proof}  By induction on the !!{derivation} of $P \aconvone Q$.  \begin{enumerate}  \item If the last rule is \olref{defn:aconvone4}, then $P$ is of the    form $\lambd[x][N]$ and $Q$ of the form    $\lambd[y][\Subst{N}{y}{x}]$, with $x \neq y$, $y \notin \FV{N}$    and $\Subst{N}{y}{x}$ defined. We distinguish cases according to    whether $x \in \FV{N}$:    \begin{enumerate}    \item If $x \in FV(N)$, then:      \begin{align*}        \FV{\lambd[y][\Subst{N}{y}{x}]} &=        \FV{\Subst{N}{y}{x}} \setminus \{y\} \\        & = ((\FV{N} \setminus \{x\}) \cup \{y\}) \setminus \{y\}         && \text{ by \olref[sub]{thm:infv}} \\        & = \FV{N} \setminus \{x\} \\        & = \FV{\lambd[x][N]}      \end{align*}    \item If $x \notin FV(N)$, then:      \begin{align*}        \FV{\lambd[y][\Subst{N}{y}{x}]}        & = FV{\Subst{N}{y}{x}} \setminus \{y\} \\        & = \FV{N} \setminus \{x\}         && \text{by \olref[sub]{thm:notinfv}} \\        & = \FV{\lambd[x][N]}.      \end{align*}    \end{enumerate}  \item The other three cases are left as exercises.   \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][alp]{lem:fv-one}.\end{prob}\begin{lem}\ollabel{lem:inv}  If $P \aconvone Q$ then $Q \aconvone P$.\end{lem}\begin{proof}  Induction on the !!{derivation} of $P \aconvone Q$.  \begin{enumerate}  \item If the last rule is \olref{defn:aconvone4}, then $P$ is of the    form $\lambd[x][N]$ and $Q$ of the form    $\lambd[y][\Subst{N}{y}{x}]$, where $x \neq y$, $y \notin \FV{N}$    and $\Subst{N}{y}{x}$ defined. First, we have $y \notin    \FV{\Subst{N}{y}{x}}$ by \olref[sub]{thm:clr}. By    \olref[sub]{thm:inv} we have that $\Subst{\Subst{N}{y}{x}}{x}{y}$ is    not only defined, but also equal to~$N$. Then by    \olref{defn:aconvone4}, we have $\lambd[y][\Subst{N}{y}{x}]    \aconvone \lambd[x][\Subst{\Subst{N}{y}{x}}{x}{y}] =    \lambd[x][N]$.  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][alp]{lem:inv}\end{prob}\begin{thm}  $\alpha$-Conversion is an equivalence relation on terms, i.e., it is  reflexive, symmetric, and transitive.\end{thm}\begin{proof}  \begin{enumerate}  \item For each term $M$, $M$ can be changed to $M$ by    \emph{zero} changes of bound variables.  \item If $P$ is $\alpha$-converts to $Q$ by a series of changes    of bound variables, then from $Q$ we can just inverse these    changes (by \olref{lem:inv}) in    opposite order to obtain~$P$.  \item If $P$ $\alpha$-converts to $Q$ by a series of changes of    bound variables, and $Q$ to $R$ by another series, then we can    change $P$ to $R$ by first applying the first series and then the    second series.  \end{enumerate}\end{proof}From now on we say that $M$ and $N$ are \emph{$\alpha$-equivalent}, $M\aeq N$, iff $M$ $\alpha$-converts to $N$ (which, as we've just shown,is the case iff $N$ $\alpha$-converts to~$M$).\begin{thm}\ollabel{thm:fv}  If $M \aeq N$, then $\FV{M} = \FV{N}$.\end{thm}\begin{proof}  Immediate from \olref{lem:fv-one}.\end{proof}\begin{lem}\ollabel{lem:sub:R}  If $R \aeq R'$ and $\Subst{M}{R}{y}$ is defined, then $\Subst{M}{R'}{y}$ is  defined and $\alpha$-equivalent to $\Subst{M}{R}{y}$.\end{lem}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[lam][syn][alp]{lem:sub:R}.\end{prob}Recall that in \olref[sub]{sec}, substitution is undefined in somecases; however, using $\alpha$-conversion on terms, we can makesubstitution always defined by renaming bound variables. The resultpreserves $\alpha$-equivalence, as shown in this theorem:\begin{thm}\ollabel{thm:sub}  For any $M$, $R$, and~$y$, there exists $M'$ such that $M \aeq M'$  and $\Subst{M'}{R}{y}$ is defined. Moreover, if there is another  pair $M'' \aeq M$ and $R''$ where $\Subst{M''}{R''}{y}$ is defined  and $R'' \aeq R$, then $\Subst{M'}{R}{y} \aeq \Subst{M''}{R''}{y}$.\end{thm}\begin{proof}  By induction on the formation of $M$:  \begin{enumerate}  \item $M$ is a variable~$z$: Exercise.  \item Suppose $M$ is of the form $\lambd[x][N]$.  Select a variable    $z$ other than $x$ and $y$ and such that $z \notin \FV{N}$ and $z    \notin \FV{R}$.  By inductive hypothesis, we there is $N'$ such    that $N' \aeq N$ and $\Subst{N'}{z}{x}$ is defined. Then    $\lambd[x][N] \aeq \lambd[x][N']$ too, by    \olref{defn:aconvone}\olref{defn:aconvone1}.  Now $\lambd[x][N']    \aeq \lambd[z][\Subst{N'}{z}{x}]$ by    \olref{defn:aconvone}\olref{defn:aconvone4}.  We can do this    because $z \ne x$, $z \notin FV(N')$ and $\Subst{N'}{z}{x}$ is    defined. Finally, $\Subst{\lambd[z][\Subst{N'}{z}{x}]}{R}{y}$ is    defined, because $z \neq y$ and $z \notin FV(R)$.    Moreover, if there is another $N''$ and $R''$ satisfying the same    conditions,    \begin{multline*}      \Subst{(\lambd[z][\Subst{N''}{z}{x}])}{R''}{y} =\\    \begin{aligned}      &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R''}{y}] \\      &= \lambd[z][\Subst{\Subst{N''}{z}{x}}{R}{y}] && \text{by        \olref{lem:sub:R}}\\      &=\lambd[z][\Subst{\Subst{N'}{z}{x}}{R}{y}]      && \text{by inductive        hypothesis}\\      &=\Subst{(\lambd[z][\Subst{N'}{z}{x}])}{R}{y}    \end{aligned}    \end{multline*}    \item $M$ is of the form $(PQ)$: Exercise.  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][syn][alp]{thm:sub}.\end{prob}\begin{cor}\ollabel{cor:sub}  For any $M$, $R$, and~$y$, there exists a pair of $M'$ and $R'$  such that $M' \aeq M$, $R \aeq R'$ and $\Subst{M'}{R'}{y}$ is  defined. Moreover, if there is another pair $M'' \aeq M$ and $R''$  with $\Subst{M'}{R'}{y}$ defined, then $\Subst{M'}{R'}{y} \aeq  \Subst{M''}{R''}{y}$.\end{cor}\begin{proof}  Immediate from \olref{thm:sub}.\end{proof}\end{document}

content/lambda-calculus/syntax/de-bruijn.tex

% Part: lambda-calculus% Chapter: syntax% Section: de-bruijn\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{deb}\olsection{The De Bruijn Index}$\alpha$-Equivalence is very natural, as terms that are$\alpha$-equivalent ``mean the same.'' In fact, it is possible to givea syntax for lambda terms which does not distinguish terms that can be$\alpha$-converted to each other. The best known replaces variables bytheir \emph{De Bruijn index}.When we write $\lambd[x][M]$, we explicitly state that $x$ is theparameter of the function, so that we can use $x$ in $M$ to refer tothis parameter. In the de Bruijn index, however, parameters have noname and reference to them in the function body is denoted by a numberdenoting the levels of abstraction between them. For example, considerthe example of $\lambd[x][\lambd[y][y x]]$: the outer abstraction is onbinds the variable~$x$; the inner abstraction binds the variableis~$y$; the sub-term $y x$ lies in the scope of the inner abstraction:there is no abstraction between $y$ and its abstract~$\lambd[y]$, butone abstract between $x$ and its abstract~$\lambd[x]$. Thus we write$0\, 1$ for $y x$, and $\lambd[][\lambd[][01]]$ for the entire term.\begin{defn}  De Bruijn terms are inductively defines as follows:  \begin{enumerate}  \item $n$, where $n$ is any natural number.  \item $PQ$, where $P$ and $Q$ are both De Bruijn terms.  \item $\lambd[][N]$, where $N$ is a De Bruijn term.  \end{enumerate}\end{defn}A formalized translation from ordinary lambda terms to De Bruijnindexed terms is as follows:\begin{defn}  \begin{align*}    F_\Gamma(x) &= \Gamma(x) \\    F_\Gamma(PQ) &= F_\Gamma(P)F_\Gamma(Q) \\    F_\Gamma(\lambd[x][N]) &= \lambd[][F_{x,\Gamma}(N)]  \end{align*}  where $\Gamma$ is a list of variables indexed from zero, and  $\Gamma(x)$ denotes the position of the variable $x$ in $\Gamma$.  For example, if $\Gamma$ is $x,y,z$, then $\Gamma(x)$ is $0$ and  $\Gamma(z)$ is $2$.    $x,\Gamma$ denotes the list resulted from pushing $x$ to the head of  $\Gamma$; for instance, continuing the $\Gamma$ in last example,  $w,\Gamma$ is $w,x,y,z$.\end{defn}Recovering a standard lambda term from a de Bruijn term is done asfollows:\begin{defn}  \begin{align*}    G_\Gamma(n) &= \Gamma[n] \\    G_\Gamma(PQ) &= G_\Gamma(P) G_\Gamma(Q) \\    G_\Gamma(\lambd[][N]) &= \lambd[x][G_{x,\Gamma}(N)]  \end{align*}  where $\Gamma$ is again a list of variables indexed from zero, and  $\Gamma[n]$ denotes the variable in position~$n$. For example,  if $\Gamma$ is $x,y,z$, then $\Gamma[1]$ is $y$.  The variable $x$ in last equation is chosen to be any variable that  not in $\Gamma$.\end{defn}Here we give some results without proving them:\begin{prop}  If $M \aconvone M'$, and $\Gamma$ is any list containing $\FV{M}$, then  $F_\Gamma(M) \eqs F_\Gamma(M')$.\end{prop}\end{document}

content/lambda-calculus/syntax/term-revisited.tex

% Part: lambda-calculus% Chapter: introduction% Section: term-revisited\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{tr}\olsection{Terms as $\alpha$-Equivalence Classes}From now on, we will consider terms up to $\alpha$-equivalence.  Thatmeans when we write a term, we mean its $\alpha$-equivalance class itis in. For example, we write $\lambd[a][\lambd[b][a c]]$ for the setof all terms $\alpha$-equivalent to it, such as $\lambd[a][\lambd[b][a    c]]$, $\lambd[b][\lambd[a][b c]]$, etc.Also, while in previous sections letters such as $N, Q$ are used todenote a term, from now on we use them to denote a class, and it isthese classes instead of terms that will be our subjects of study inwhat follows. Letters such as $x, y$ continues to denote a variable.We also adopt the notation $\rep{M}$ to denote an arbitrary!!{element} of the class~$M$, and $\rep{M}[0], \rep{M}[1], etc. $ ifwe need more than one.We reuse the notations from terms to simplify our wording. Wehave following definition on classes:\begin{defn}  \begin{enumerate}  \item $\lambd[x][N]$ is defined as the class containing    $\lambd[x][\rep{N}]$.  \item $PQ$ is defined to be the class containing $\rep{P}\rep{Q}$.  \end{enumerate}\end{defn}It is not hard to see that they are well defined, because$\alpha$-conversion is compatible.\begin{defn} \ollabel{def:fv}  The \emph{free variables} of an $\alpha$-equivalence class~$M$, or  $FV(M)$, is defined to be $FV(\rep{M})$.\end{defn}This is well defined since $FV(\rep{M}[0]) =FV(\rep{M}[1])$, as shown in \olref[alp]{thm:fv}.We also reuse the notation for substition into classes:\begin{defn} \ollabel{def:sub}  The \emph{substitution} of $R$ for $y$ in $M$, or $\Subst{M}{R}{y}$, is  defined to be $\Subst{\rep{M}}{\rep{R}}{y}$, for any $\rep{M}$ and  $\rep{R}$ making the substition defined.\end{defn}This is also well defined as shown in \olref[alp]{cor:sub}.Note how this definition significantly simplifies our reasoning. Forexample:\begin{align}  \Subst{\lambd[x][x]}{y}{x} & =\ollabel{eq:1}\\  &= \Subst{\lambd[z][z]}{y}{x} \ollabel{eq:2}\\  &= \lambd[z][\Subst{z}{y}{x}] \\  &= \lambd[z][z]\end{align}\olref{eq:1} is undefined if we still regard it as substitution onterms; but as mentioned earlier, we now consider it a substitution onclasses, which is why \olref{eq:2} can happen: we can replace$\lambd[x][x]$ with $\lambd[z][z]$ because they belong to the sameclass.For the same reason, from now on we will assume that therepresentatives we choose always satisfy the conditions needed forsubstitution. For example, when we see $\Subst{\lambd[x][N]}{R}{y}$,we will assume the representative $\lambd[x][N]$ is chosen so that$x \neq y$ and $x \notin FV(R)$.Since it is a bit strange to call $\lambd[x][x]$ a ``class'', let'scall them $\Lambda$-terms (or simply ``terms'' in the rest of thepart) from now on, to distinguish them from $\lambda$-terms that weare familiar with.\begin{editorial}  We cannot say goodbye to terms yet: the whole definition of  $\Lambda$-terms is based on $\lambda$-terms, and we haven't provided  a method to define functions on $\Lambda$-terms, which means all  such functions have to be first defined  on $\lambda$-terms, and  then ``projected'' to $\Lambda$-terms, as we did for substitutions.  However we assume the reader can intuitively understand how we can  define functions on $\Lambda$-terms.\end{editorial}\end{document}

content/lambda-calculus/syntax/beta.tex

% Part: lambda-calculus% Chapter: introduction% Section: beta\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{int}{bet}\olsection{$\beta$-reduction}When we see $(\lambd[m][(\lambd[y][y]) m])$, it is natural toconjecture that it has some connection with $\lambd[m][m]$, namely thesecond term should be the result of ``simplifying'' the first.  Thenotion of \emph{$\beta$-reduction} captures this intuition formally.\begin{defn}[$\beta$-contraction, $\bredone$] \ollabel{defn:betacontr}  \emph{The $\beta$-contraction} ($\bredone$) is the smallest compatible  relation on terms satisfying the following condition:  \[    (\lambd[x][N])Q \bredone \Subst{N}{Q}{x}   \]  We say $P$ is \emph{$\beta$-contracted} to $Q$ if $P \bredone Q$.  A  term of the form $(\lambd[x][N])Q$ is called a \emph{redex}.\end{defn}\begin{prob} \ollabel{prob:def}  Spell out the equivalent inductive definitions of $\beta$-contraction as we  did for change of bound variable in \olref[lam][syn][alp]{defn:aconvone}.\end{prob}  \begin{defn}[$\beta$-reduction, $\bred$] \ollabel{defn:betared}  \emph{$\beta$-reduction} ($\bred$) is the smallest reflexive,  transitive relation on terms containing $\bredone$.  We say $P$ is  $\beta$-reduced to $Q$ if $P \bred Q$.\end{defn}We will write $\redone$ instead of $\bredone$, and $\red$ instead of$\bred$ when context is clear.Informally speaking, $M \bred N$  if and only if $M$ can be changed to$N$ by zero or several steps of $\beta$-contraction.\begin{defn}[$\beta$-normal]A term that cannot be $\beta$-contracted any further is said to be\emph{$\beta$-normal}. \end{defn}If $M \bred N$ and $N$ is $\beta$-normal, then we say $N$ is a\emph{normal form} of~$M$. One may ask if the normal form of a term isunique, and the answer is yes, as we will see later.Let us consider some examples.\begin{enumerate}\item We have\begin{align*}(\lambd[x][xxy]) \lambd[z][z] & \redone (\lambd[z][z])(\lambd[z][z]) y \\& \redone (\lambd[z][z]) y \\& \redone y\end{align*}\item ``Simplifying'' a term can actually make it more complex:\begin{align*}(\lambd[x][xxy])(\lambd[x][xxy]) & \redone (\lambd[x][xxy])(\lambd[x][xxy])y \\& \redone (\lambd[x][xxy])(\lambd[x][xxy])yy \\& \redone \dots\end{align*}\item It can also leave a term unchanged:\[(\lambd[x][xx])(\lambd[x][xx]) \redone (\lambd[x][xx])(\lambd[x][xx])\]\item Also, some terms can be reduced in more than one way; for  example,\[(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[y][yv]) z\]by contracting the outermost application; and\[(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[x][zx]) v\]by contracting the innermost one. Note, in this case, however, thatboth terms further reduce to the same term, $zv$.\end{enumerate}The final outcome in the last example is not a coincidence, but ratherillustrates a deep and important property of the lambda calculus, known as theChurch--Rosser property.\begin{digress}  In general, there is more than one way to $\beta$-reduce a term,  thus many reduction strategies have been invented, among which the  most common is the \emph{natural strategy}.  The natural strategy  always contracts the \emph{left-most} redex, where the position of a  redex is defined as its starting point in the term.  The natural  strategy has the useful property that a term can be reduced to a  normal form by some strategy iff it can be reduced to normal form  using the natural strategy. In what follows we will use the natural  stratuegy unless otherwise specified.\end{digress}\begin{defn}[$\beta$-equivalence, $\equal$]  \emph{$\beta$-Equivalence} ($\equal$) is the relation inductively  defined as follows:  \begin{enumerate}  \item $M \equal M$.  \item If $M \equal N$, then $N \equal M$.  \item If $M \equal N$, $N \equal O$, then $M \equal O$.  \item If $M \equal N$, then $PM \equal PN$.  \item If $M \equal N$, then $MQ \equal NQ$.  \item If $M \equal N$, then $\lambd[x][M] \equal \lambd[x][N]$.  \item $(\lambd[x][N])Q \equal \Subst{N}{Q}{x}$.  \end{enumerate}\end{defn}The first three rules make the relation an equivalence relation; thenext three make it compatible; the last ensures that it contains$\beta$-contraction.Informally speaking, two terms are $\beta$-equivalent if and only ifone of them can be changed to the other in zero or more steps of$\beta$-contraction, or ``inverse'' of $\beta$-contraction. The inverse of$\beta$-contraction is defined so that $M$ inverse-$\beta$-contracts to $N$iff $N$ $\beta$-contracts to $M$.Besides the above rules, we will extend the relation with morerules, and denote the extended equivalence relation as $\equal[X]$,where $X$ is the extending rule.\end{document}

content/lambda-calculus/syntax/eta.tex

% Part: lambda-calculus% Chapter: syntax% Section: eta\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{syn}{eta}\olsection{$\eta$-conversion}There is another relation on $\lambda$ terms. In \olref[fv]{sec} weused the example $\lambd[x][(fx)]$, which accepts an argument andapplies $f$ to it.  In other words, it is the same function as~$f$:$\lambd[x][(fx)]N$ and $fN$ both reduce to~$fN$.  We use$\eta$-reduction (and $\eta$-extension) to capture this idea.\begin{defn}[$\eta$-contraction, $\eredone$]  \ollabel{defn:beredone}  \emph{$\eta$-contraction} ($\eredone$) is the smallest compatible relation  on terms satisfying the following condition:  \[    \lambd[x][M x] \eredone M \text{ provided } x \notin FV(M)  \]\end{defn}\begin{defn}[$\beta\eta$-reduction, $\bered$] \ollabel{defn:bered}  \emph{$\beta\eta$-reduction} ($\bered$) is the smallest reflexive,  transitive relation on terms containing $\bredone$ and $\eredone$,  i.e., the rules of reflexivity and transitive plus the following two  rules:  \begin{enumerate}  \item If $M \bredone N$ then $M \bered N$. \ollabel{defn:bered3}  \item If $M \eredone N$ then $M \bered N$. \ollabel{defn:bered4}  \end{enumerate}    \end{defn}\begin{defn}  We extend the equivalence relation $\equal$ with the $\eta$-conversion rule:  \[  \lambd[x][f x] \equal f  \]  and denote the extended relation as $\equal[\eta]$.\end{defn}$\eta$-equivalence is important because it is related to extensionalityof lambda terms:\begin{defn}[Extensionality]  We extend the equivalence relation $\equal$ with the (\ext) rule:  \begin{center}  If $Mx \equal Nx$ then $M \equal N$, provided $x \notin FV(MN)$.  \end{center}  and denote the extended relation as $\equal[\ext]$.\end{defn}Roughly speaking, the rule states that two terms, viewed as functions,should be considered equal if they behave the same for the sameargument.We now prove that the $\eta$ rule provides exactly the extensionality,and nothing else.\begin{thm}  $M \equal[\ext] N$ if and only if $M \equal[\eta] N$.\end{thm}\begin{proof}  First we prove that $\equal[\eta]$ is closed under the  extensionality rule. That is, $ext$ rule doesn't add anything to  $\equal[\eta]$. We then have $\equal[\eta]$ contains $\equal[\ext]$,  and if $M \equal[\ext] N$, then $M \equal[\eta] N$.  To prove $\equal[\eta]$ is closed under \ext, note that for any $M  \equal N$ derived by the \ext{} rule, we have $Mx  \equal[\eta] Nx$ as premise. Then we have $\lambd[x][Mx]  \equal[\eta] \lambd[x][Nx]$ by a rule of $\equal$, applying $\eta$  on both side gives us $M \equal[\eta] N$.  Similarly we prove that the $\eta$ rule is contained in  $\equal[ext]$. For any $\lambd[x][Mx]$ and $M$ with $x \notin  FV(M)$, we have that $(\lambd[x][Mx])x \equal[\ext] Mx$,  giving us $\lambd[x][Mx] \equal[\ext] M$ by the \ext{} rule.\end{proof}\end{document}