PCF.tex

\section{The Language PCF}\label{sec:pcf}

PCF stands for ``programming with computable functions.'' It is based on LCF, the ``logic of computable functions,'' which was introduced by Dana Scott in \cite{LCF} as a restricted formalism for investigating computation, one better suited to this task than set theory. Gordon Plotkin then introduced PCF in \cite{PCF} in order to investigate the semantics of programming languages. He named this language PCF because it was inspired by the syntax of LCF. In what follows, we give a quick introduction to the language PCF. The reader may consult \cite{LambdaNotes} for a more detailed introduction.

\subsection{Types and Terms}

PCF is a programming language that is very similar to the simply-typed lambda calculus. Instead of type variables, it has concrete types $\mbf{bool}$ and $\mbf{nat}$. It also has the classical type constructors $\to$, $\times$ and $1$. Formally, types are defined by the following BNF:

\[ A, B := \mbf{bool} \sep \mbf{nat} \sep A\to B \sep A\times B \sep 1. \]

The terms for PCF are those of the simply-typed lambda calculus, plus some concrete terms. In BNF:

\begin{align*}
    M, N, P := x &\sep MN \sep \lambda x^A.M \sep \langle M, N\rangle \sep \pi_1M \sep \pi_2M \sep * \\
    &\sep \mbf{T} \sep \mbf{F} \sep \mbf{zero} \sep \mbf{succ}\,(M) \sep \mbf{pred}\,(M) \\
    &\sep \mbf{iszero}\,(M) \sep \mbf{if}\,M\,\mbf{then}\,N\,\mbf{else}\,P \sep \mbf{Y}(M).
\end{align*}

The $\mbf{Y}$ constructor returns a fixpoint of the given term. It is what makes the language Turing complete. Without adding $\Y$ to PCF, we would be able to prove that every well-typed term eventually reduces to a term that cannot be reduced further. That is, without $\Y$, every program written in PCF halts, but there are computable functions that do not halt on some inputs, so PCF without $\Y$ cannot be Turing complete. An example of how $\Y$ produces non-halting PCF programs is given by $\Y(\lambda x^{\textbf{nat}}. \textbf{succ } x),$ whose reduction never halts:

% Reducing (lambda x . succ x) to succ makes this easier to read, but is succ a term of PCF?

$$\Y(\lambda x^{\textbf{nat}}. \textbf{succ } x) \to^* \textbf{succ}(\Y(\lambda x^{\textbf{nat}}. \textbf{succ } x)) \to^* \succ(\succ(\Y(\lambda x^{\textbf{nat}}. \textbf{succ } x))) \to^* ... .$$

One may think of $\Y$ as a way to introduce recursion into PCF. For example, the addition function is most naturally defined by recursion, and it can be defined using $\Y$ as follows:

\[ + := \Y(\lambda f^{\mbf{nat}\to\mbf{nat}}m^\mbf{nat}n^\mbf{nat}.\mbf{if}\,\mbf{iszero}(m)\,\mbf{then}\,n\,\mbf{else }\,\mbf{succ}(f \mbf{pred}(m) n)). \]

\subsection{Typing Rules}

The reader may notice that among the well-formed terms, some do not make any sense. Such terms are, for example, $\mbf{iszero}(\mbf{T})$ or $\pi_1(\lambda x^\mbf{nat}.x)$. We should thus specify a type for each term and specify which constructions can be applied to which types. We start by giving the typing rules for the fragment of PCF that is the simply-typed lambda calculus with finite products:

\begin{multicols}{2}
    
    \begin{prooftree} % unit
    \AxiomC{}
    \UnaryInfC{$\Gamma \proves * : 1$}
    \end{prooftree}
    
    \begin{prooftree} % var
    \AxiomC{}
    \UnaryInfC{$\Gamma, x:A \proves x:A$}
    \end{prooftree}
    
    \begin{prooftree} % abs
    \AxiomC{$\Gamma, x:A\proves M:B$}
    \UnaryInfC{$\Gamma\proves\lambda x^A.M : A\to B$}
    \end{prooftree}
    
    \begin{prooftree} % app
    \AxiomC{$\Gamma\proves M:A\to B\qquad \Gamma\proves N:A$}
    \UnaryInfC{$\Gamma\proves MN:B$}
    \end{prooftree}
    
    \begin{prooftree} % pair
    \AxiomC{$\Gamma\proves M:A\qquad\Gamma\proves N:B$}
    \UnaryInfC{$\Gamma\proves \langle M,N\rangle:A\times B$}
    \end{prooftree}
    
    \begin{prooftree} % pi_1
    \AxiomC{$\Gamma\proves M:A\times B$}
    \UnaryInfC{$\Gamma\proves\pi_1M:A$}
    \end{prooftree}
    
    
    
    \begin{prooftree} % pi_2
    \AxiomC{$\Gamma\proves M:A\times B$}
    \UnaryInfC{$\Gamma\proves\pi_2M:B.$}
    \end{prooftree}
    
    
\end{multicols}

We now give the typing rules for the rest of PCF:

\begin{multicols}{2}
    \begin{prooftree} % T
    \AxiomC{}
    \UnaryInfC{$\Gamma \proves \mathbf{T} : \mathbf{bool}$}
    \end{prooftree}
    
    \begin{prooftree} % zero
    \AxiomC{}
    \UnaryInfC{$\Gamma \proves \mathbf{zero} : \mathbf{nat}$}
    \end{prooftree}
    
    \begin{prooftree} % pred
    \AxiomC{$\Gamma \proves M : \mathbf{nat}$}
    \UnaryInfC{$\Gamma \proves \mathbf{pred}(M) : \mathbf{nat}$}
    \end{prooftree}
    
    \begin{prooftree} % if-then-else
    \AxiomC{$\Gamma \proves M : \mathbf{bool}\qquad\Gamma \proves N : A\qquad\Gamma \proves P : A$}
    \UnaryInfC{$\Gamma \proves \textbf{if } M \textbf{ then } N \textbf{ else } P : A$}
    \end{prooftree}

    \begin{prooftree} % F
    \AxiomC{}
    \UnaryInfC{$\Gamma \proves \mathbf{F} : \mathbf{bool}$}
    \end{prooftree}
    
    \begin{prooftree} % succ
    \AxiomC{$\Gamma \proves M : \mathbf{nat}$}
    \UnaryInfC{$\Gamma \proves \mathbf{succ}(M) : \mathbf{nat}$}
    \end{prooftree}
    
    \begin{prooftree} % iszero
    \AxiomC{$\Gamma \proves M : \mathbf{nat}$}
    \UnaryInfC{$\Gamma \proves \mathbf{iszero}(M) : \mathbf{bool}$}
    \end{prooftree}
    
    \begin{prooftree} % Y
    \AxiomC{$\Gamma \proves M : A \to A$}
    \UnaryInfC{$\Gamma \proves \mathbf{Y}(M) : A.$}
    \end{prooftree}
\end{multicols}

\subsection{Reduction}

PCF is a programming language in which PCF-terms are programs. How do we run such a program? We reduce it to its simplest form. Note that the syntax of a PCF-term is not sufficient to determine its reduction behavior. For example, we have two sensible ways to reduce the term $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero)),$ as shown below: 

\[
\begin{tikzcd}[ampersand replacement=\&]
\& \mathbf{pred} (\mathbf{succ} ((\lambda x^{\textbf{nat}}.x)\mathbf{zero})) \ar[ld] \ar[rd]\& \\
(\lambda x^{\textbf{nat}}.x)\textbf{zero} \ar[rd] \& \& \textbf{pred} ( \textbf{succ} (\mathbf{zero})) \ar[ld] \\
\& \textbf{zero} \& \\
\end{tikzcd}
\]

In order to view PCF-terms as programs, we need to specify a reduction order for PCF-terms so that they can be run deterministically. This reduction order is what makes PCF a programming language, rather than just a calculus like the simply-typed lambda calculus. Below, we specify this reduction order in in the small-step reduction style, while noting that it is also possible to do this in a big-step reduction style.

%%%%% small-step for simply-typed lambda calculus

Small-step reduction specifies how to reduce a PCF-term one step at a time. For example, the reduction $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero)) \to \pred(\succ(\zero))$ is one small-step reduction that the rules below specify. If we reduce once more, $\pred(\succ(\zero)) \to \zero$, we arrive at the \textit{value} $\zero$, which we think of as the result of running the program $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero)).$ In general, the form of values is given by the following BNF, where $M$ and $N$ are any PCF-terms:
$$ V := \T \sep \F \sep \zero \sep \succ(V) \sep * \sep \langle M,N \rangle \sep \lambda x^A.M.$$

We begin by giving the small-step reduction rules for the fragment of PCF that is the simply-typed lambda calculus with finite products:

\begin{multicols}{2}

% small-step unit
\begin{prooftree}
\AxiomC{$M : 1$}
\AxiomC{$M \neq *$}
\BinaryInfC{$M \to *$}
\end{prooftree}

% small-step functions
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$(\lambda x^A . M)N \to M[N/x]$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \to N$}
\UnaryInfC{$MP \to NP$}
\end{prooftree}

%small-step products
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\pi_1 \langle M_1,M_2 \rangle \to M_1$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\pi_2 \langle M_1, M_2 \rangle \to M_2$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \to N$}
\UnaryInfC{$\pi_i M \to \pi_i N.$}
\end{prooftree}
\end{multicols}

We now give the small-step reduction rules for the rest of PCF:

\begin{multicols}{2}
%%%%% small-step for PCF

%small-step Y
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\Y(M) \to M(\Y(M))$}
\end{prooftree}

%small-step succ
\begin{prooftree}
\AxiomC{$M \to N$}
\UnaryInfC{$\succ(M) \to \succ(N)$}
\end{prooftree}




%small-step pred
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\pred (\zero) \to \zero$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \to N$}
\UnaryInfC{$\pred(M) \to \pred(N)$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\pred(\succ(V)) \to V$}
\end{prooftree}

%small-step iszero
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\iszero (\zero) \to \T$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \to N$}
\UnaryInfC{$\iszero(M) \to \iszero(N)$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\iszero(\succ(V)) \to \F$}
\end{prooftree}



% small-step if then else
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\textbf{if } \T \textbf{ then } N \textbf{ else } P \to N$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\textbf{if } \F \textbf{ then } N \textbf{ else } P \to P$}
\end{prooftree}

\end{multicols}

\begin{prooftree}
\AxiomC{$M \to M'$}
\UnaryInfC{$\textbf{if } M \textbf{ then } N \textbf{ else } P \to \textbf{if } M' \textbf{ then } N \textbf{ else }P.$}
\end{prooftree}



Small-steps can be concatenated. For example, the small-steps $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero)) \to \pred(\succ(\zero)) \to \zero$ can be concatenated to $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero)) \to^* \zero,$ where $\to^*$ denotes finitely many small-step reductions. Since $\zero$ is a value, we say that $\pred(\succ((\lambda x^{\textbf{nat}}.x)\zero))$ \textit{evaluates} to $\zero.$ In general, if $M \to^* V$, where $V$ is a value, we say that $M$ evaluates to $V.$

The notion of evaluating to a value is what gives us the big-step style of specifying reduction order. We can give rules that directly axiomatize big-step reduction, usually denoted by $\Downarrow,$ with the intention that $\Downarrow$ coincides with evaluating to a value via $\to^*.$ We will not give the rules for $\Downarrow,$ however, because our implementation of big-step reduction in Idris closely follows the idea that a big-step is composed of multiple small-steps that result in a value.


\begin{comment}
%%%%% big-step for simply-typed lambda calculus

\begin{multicols}{2}

%big-step unit
\begin{prooftree}
\AxiomC{$M : 1$}
\UnaryInfC{$M \Downarrow *$}
\end{prooftree}

%big-step function
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\lambda x^A.M \Downarrow \lambda x^A .M$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow \lambda x^A. M'$}
\AxiomC{$M'[N/x]\Downarrow V$}
\BinaryInfC{$MN \Downarrow V$}
\end{prooftree}

\columnbreak
% big-step product
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\langle M,N \rangle \Downarrow \langle M,N \rangle$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow \langle M_1,M_2 \rangle$}
\AxiomC{$M_1 \Downarrow V$}
\BinaryInfC{$\pi_1 M \Downarrow V$}
\end{prooftree}



\begin{prooftree}
\AxiomC{$M \Downarrow \langle M_1,M_2 \rangle $}
\AxiomC{$M_2 \Downarrow V$}
\BinaryInfC{$\pi_2 M \Downarrow V$}
\end{prooftree}
\end{multicols}

We now give the big-step reduction rules for the rest of PCF:

%%%%% big-step for PCF 

\begin{multicols}{2}

% big-step Y
\begin{prooftree}
\AxiomC{$M(\mathbf{Y}(M)) \Downarrow V$}
\UnaryInfC{$\mathbf{Y}(M) \Downarrow V$}
\end{prooftree}

% big-step boolean
\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\mathbf{T} \Downarrow \mathbf{T}$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\UnaryInfC{$\textbf{F} \Downarrow \textbf{F}$} 
\end{prooftree}

% big-step nat succ
\begin{prooftree}
\AxiomC{\text{}}
\UnaryInfC{$\textbf{zero} \Downarrow \mathbf{zero}$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow V$}
\UnaryInfC{$\succ (M) \Downarrow \succ (V)$}
\end{prooftree}

% big-step nat pred
\begin{prooftree}
\AxiomC{$M \Downarrow \mathbf{zero}$}
\UnaryInfC{$\mathbf{pred}(M) \Downarrow \mathbf{zero}$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow \mathbf{succ}(V)$}
\UnaryInfC{$\mathbf{pred}(M) \Downarrow V$}
\end{prooftree}

% big-step iszero
\begin{prooftree}
\AxiomC{$M \Downarrow \mathbf{zero}$}
\UnaryInfC{$\mathbf{iszero}(M) \Downarrow \mathbf{T}$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow \mathbf{succ}(V)$}
\UnaryInfC{$\mathbf{iszero}(M) \Downarrow \mathbf{F}$}
\end{prooftree}

% big-step if then else
\begin{prooftree}
\AxiomC{$M \Downarrow \T$}
\AxiomC{$N \Downarrow V$}
\BinaryInfC{$\textbf{if } M \textbf{ then } N \textbf{ else } P \Downarrow V$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$M \Downarrow \F$}
\AxiomC{$P \Downarrow V$}
\BinaryInfC{$\textbf{if } M \textbf{ then } N \textbf{ else } P \Downarrow V$}
\end{prooftree}

\end{multicols}

\end{comment}