Conversion operations of the lambda-calculus

Abstract

This note provides a super lightweight explanation of the three conversion operations of the $\lambda$-calculus known (cryptically) as $\alpha$, $\beta$ and $\eta$ conversions respectively (borrowed fairly freely from the delightful reference given at the bottom.)

Syntax vs. semantics

The $\textbf{syntax}$ of the language of $\textit{$\lambda$- expressions}$ is \[ \begin{eqnarray} <exp> & ::= & <constant>\;\; & \text{Constants} \nonumber \\ & \mid & <variable>\;\; & \text{Variables} \nonumber \\ & \mid & <exp> <exp>\;\; & \text{Applications} \nonumber \\ & \mid & \lambda<variable>.<exp>\;\; & \text{Abstractions} \nonumber \end{eqnarray} \] The $\textbf{semantics}$ of the the $\lambda$-calculus is defined by three $\textit{conversion rules}$. To understand them requires the terminology of $\textit{free}$ and $\textit{bound}$ variables. An occurence of a variable in a $\lambda$-expression is bound if there is an enclosing abstraction that binds it, and is free otherwise. For example, in $\lambda x.+\; ((\lambda y. +\;y\; z)\;7)\;x$, $x$ and $y$ appear bound whereas $z$ appears free.

$\beta$-conversion

$\beta$-reduction describes how to apply a function to an argument. For example, $\left(\lambda x.+\;x\;1\right)\; 4$ denotes the application of a particular $\lambda$-abstraction to the argument $4$. The result of applying a $\lambda$-abstraction to an argument is an instance of the body of the $\lambda$-abstraction in which (free) occurences of the formal parameter in the body are replaced with (copies of) the argument. Thus, $\left(\lambda x.+\;x\;1\right)\; 4 \rightarrow +\;4\;1 \rightarrow 5$. In the event there are no occurences of the formal parameter in the abstraction body, the argument is discarded unused so, $(\lambda x.\;3)\;4 \rightarrow 3$. Care is needed when formal parameter names are not unique. For example, \[ \begin{eqnarray} & & \left(\lambda x.\;\left(\lambda x.+ \left(-\;x\;1\right)\right)\;x\;3\right)\; 9 \nonumber \\ & \rightarrow & \left(\lambda x.+ \left(-\;x\;1\right)\right)\;9\;3 \nonumber \\ & \rightarrow & +\;\left(-\;9\;1\right)\;3 \nonumber \\ & \rightarrow & +\;8\;3 \nonumber \\ & \rightarrow & 11 \nonumber \end{eqnarray} \] The key point of that example is that we did not substitue for the inner $x$ in the first reduction because it was not free in the body of the outer $\lambda x$ abstraction. Indeed, in the OCaml top-level we observe

       # (fun x -> (fun x -> ( + ) (( - ) x 1)) x 3) 9 ;;
       - : int = 11
      

or equivalently, in C++,

      auto add = [](int x) { return [=](int y) { return x + y; }; };
      auto sub = [](int x) { return [=](int y) { return x - y; }; };
      [=](int x) { 
        return [=](int x) {
          return add (sub (x) (1)); 
          } (x) (3); 
      } (9) ; //is the value '11'
      

The $\beta$-rule applied backwards is called $\beta$-abstraction and written with a backwards reduction arrow '$\leftarrow$'. Thus, $+\;4\;1 \leftarrow (\lambda x.\;+\;1\;x)\;4$. $\beta$-conversion means reduction or abstraction and is written with a double-ended arrow augmented with a $\beta$ (in order to distinguish it from other forms of conversion). So, $+\;4\;1 \underset{\beta}{\leftrightarrow} (\lambda x.\;+\;1\;x)\;4$. One way to look at $\beta$ conversion is that it is saying something about $\lambda$-expressions that look different but mean the same thing.

$\alpha$-conversion

It seems obvious that the two abstractions $\lambda x.+\;x\;1$ and $\lambda y.+\;y\;1$ "ought" to be equivalent. $\alpha$-conversion allows us to change the name of a formal parameter as long as it is done consistently. So we write $\lambda x.+\;x\;1 \underset{\alpha}{\leftrightarrow} \lambda y.+\;y\;1$. Of course, the newly introduced name must not occur free in the body of the original $\lambda$-abstraction.

$\eta$-conversion

This last conversion rule exists to to complete our intuition about what $\lambda$-abstractions "ought" to be equivalent. The rule is this : If $f$ denotes a function, $x$ a variable that does not occur free in $f$, then $\lambda x.f\;x \underset{\eta}{\leftrightarrow} f$. For example, in OCaml if we define f by let f x = x + 1 then clearly fun x -> f x produces the same results for all values x in the domain of f.

Summary

The first section provides a set of formal rules for constructing expressions (the BNF grammar). Using the notation $E\;\left[M/x\right]$ to mean the expression $E$ with $M$ substituted for free occurrences of $x$ we can succintly state the the rules for converting one expression into an equivalent one as \[ \begin{eqnarray} x\;\left[M/x\right] & = & M \nonumber \\ c\;\left[M/x\right] & = & c\;\;\text{where $c$ is any variable or constant other than $x$} \nonumber \\ \left(E\;F\right)\;\left[M/x\right] & = & E\left[M/x\right]\; F\left[M/x\right]\; \nonumber \\ \left(\lambda x.E\right)\;\left[M/x\right] & = & \lambda x.E \nonumber \\ \left(\lambda y.E\right)\;\left[M/x\right] & & \text{where $y$ is any variable other than $x$} \nonumber \\ & = & \lambda y.E\left[M/x\right]\;\text{if $x$ does not occur free in E or $y$ does not occur free in $M$} \nonumber \\ & = & \lambda z.\left(E\left[z/y\right]\right)\left[M/x\right]\;\text{otherwise}\nonumber \\ \end{eqnarray} \]

---

References:
[1] The Implementation of Functional Programming Languages by Simon L. Peyton Jones. 1987.

The fixpoint combinator

Consider the following recursive definition of the factorial function. \[ FAC = \lambda n.\;IF \left(=\;n\;0\right)\;1\;\left(*\;n\;\left(FAC\;\left(-\;n\;1\right)\right)\right) \nonumber \] The definition relies on the ability to name a $\lambda$-abstraction and then to refer to this name inside the $\lambda$-abstraction itself. No such facility is provided by the $\lambda$-calculus. $\beta$-abstraction is applying $\beta$-reduction backwards to introduce new $\lambda$-abstractions, thus $+\;4\;1\leftarrow \left(\lambda x.\;+\;x\;1\right)\; 4$. By $\beta$-abstraction on $FAC$, its definition can be written \[ FAC = \left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right) FAC \nonumber \] This definition has taken the form $FAC = g\;FAC$ where $g = \left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right)$ is without recursion. We see also that $FAC$ is a fixed point ("fixpoint") of $g$. It is clear this fixed point can only depend on $g$ so supposing there were a function $Y$ which takes a function and delivers a fixpoint of the function as the result, we'd have $FAC = Y\;g = g\;(Y\;g)$. Under the assumption such a function exists, in order to build confidence this definition of $FAC$ works, we will try to compute $FAC\;1$. Recall \[ \begin{eqnarray} &FAC& = Y\;g \nonumber \\ &g& = \lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right) \nonumber \end{eqnarray} \] So, \[ \begin{eqnarray} FAC\;1 &\rightarrow& (Y\;g)\; 1 \nonumber \\ &\rightarrow& (g\;(Y\;g))\;1 \nonumber \\ &\rightarrow& (\left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right) (Y\;g))\; 1 \nonumber \\ &\rightarrow& \left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(\left(Y\;g\right)\;\left(-\;n\;1\right)\right)\right)\right)\; 1 \nonumber \\ &\rightarrow& *\;1\;\left(\left(Y\;g\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(g\;\left(Y\;g\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(\left(\lambda fac.\;\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(fac\;\left(-\;n\;1\right)\right)\right)\right)\right)\;\left(Y\;g\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;\left(\left(\lambda n.\;IF\left(=\;n\;0\right)\;1\;\left(*\;n\;\left(\left(Y\;g\right)\;\left(-\;n\;1\right)\right)\right)\right)\;0\right) \nonumber \\ &\rightarrow& *\;1\;1 \nonumber \\ &=& 1 \nonumber \end{eqnarray} \]

The $Y$ combinator of the $\lambda$-calculus is defined as the $\lambda$-term $Y = \lambda f.\;\left(\lambda x.\;f\;\left(x\;x\right)\right)\left(\lambda x.\;f\;\left(x\;x\right)\right)$. $\beta$ reduction of this term applied to an arbitrary function $g$ proceeds like this: \[ \begin{eqnarray} Y\;g &\rightarrow& \left(\lambda f.\;\left(\lambda x.\;f\;\left(x\;x\right)\right) \left(\lambda x.\;f\;\left(x\;x\right)\right)\right)\;g \nonumber \\ &\rightarrow& \left(\lambda x.\;g\;\left(x\;x\right)\right) \left(\lambda x.\;g\;\left(x\;x\right)\right) \nonumber \\ &\rightarrow& g\;\left(\left(\lambda x.\;g\;\left(x\;x\right)\right)\;\left(\lambda x.\;g\;\left(x\;x\right)\right)\right) \nonumber \\ &=& g\;\left(Y\;g\right) \end{eqnarray} \] The application of this term has produced a fixpoint of $g$. That is, we are satisfied that this term will serve as a definition for $Y$ having the property we need and call it the "fixpoint combinator".

In the untyped $\lambda$-calculus, $Y$ can be defined and that is sufficient for expressing all the functions that can be computed without having to add a special construction to get recursive functions. In typed $\lambda$-calculus, $Y$ cannot be defined as the term $\lambda x.\;f\;(x\;x)$ does not have a finite type. Thus, when implementing recursion in a functional programming language it is usual to implement $Y$ as a built-in function with the reduction rule $Y\;g \rightarrow g\;(Y\;g)$ or, in a strict language, $(Y\; g)\;x \rightarrow (g\;(Y\;g))\;x$ to avoid infinite recursion.

For an OCaml like language, the idea then is to introduce a built-in constant $\mathbf{Y}$ and to denote the function defined by $\mathbf{let\;rec}\;f\;x = e$ as $\mathbf{Y}(\mathbf{fun}\;f\;x \rightarrow e)$. Intuitivly, $\mathbf{Y}$ is a fixpoint operator that associates a functional $F$ of type $\alpha \rightarrow \beta$ with a fixpoint $Y(F)$ of type $\alpha \rightarrow \beta \rightarrow \alpha$, that is, a value having the property $\mathbf{Y}\;F = F\;\left(\mathbf{Y}\;F\right)$. The relevant deduction rules involving this constant are: \[ \begin{equation} \frac{\vdash f\;(Y\;f)\;x \Rightarrow v} {\vdash (Y\;f)\;x \Rightarrow v} \tag{App-rec} \end{equation} \] \[ \begin{equation} \frac{\vdash e_{2}\left[Y(\mathbf{fun}\;f\;x \rightarrow e_{1})/f\right] \Rightarrow v} {\vdash \mathbf{let\;rec}\;f\;x=e_{1}\;\mathbf{in}\;e_{2} \Rightarrow v} \nonumber \tag {Let-rec} \end{equation} \]

---

References:
[1] The Implementation of Functional Programming Languages,Simon Peyton Jones, 1987.
[2] The Functional Approach to Programming, Guy Cousineau, Michel Mauny, 1998.

Generic mappings over pairs

Browsing around on Oleg Kiselyov's excellent site, I came across a very interesting paper about "Advanced Polymorphism in Simpler-Typed Languages". One of the neat examples I'm about to present is concerned with expressing mappings over pairs that are generic not only in the datatypes involved but also over the number of arguments. The idea is to produce a family of functions $pair\_map_{i}$ such that

pair_map_1 f g (x, y) (x', y') → (f x, g y) 
pair_map_2 f g (x, y) (x', y') → (f x x', g y y') 
pair_map_3 f g (x, y) (x', y') (x'', y'', z'') → (f x x' x'', g y y' y'')
       .
       .
       .

The technique used to achieve this brings a whole bunch of functional programming ideas together : higher order functions, combinators and continuation passing style (and also leads into topics like the "value restriction" typing rules in the Hindley-Milner system).

let ( ** ) app k = fun x y -> k (app x y)
let pc k a b = k (a, b)
let papp (f1, f2) (x1, x2) = (f1 x1, f2 x2)
let pu x = x

With the above definitions, $pair\_map_{i}$ is generated like so.

(*The argument [f] in the below is for the sake of value restriction*)
let pair_map_1 f = pc (papp ** pu) (f : α -> β)
let pair_map_2 f = pc (papp ** papp ** pu) (f : α -> β -> γ)
let pair_map_3 f = pc (papp ** papp ** papp ** pu) (f : α -> β -> γ -> δ)

For example,

# pair_map_2 ( + ) ( - ) (1, 2) (3, 4) ;;
- : int * int = (4, -2)

Reverse engineering how this works requires a bit of algebra.

Let's tackle $pair\_map_{1}$. First

pc (papp ** pu) = (λk f g. k (f, g)) (papp ** pu) = λf g. (papp ** pu) (f, g)

and,

papp ** pu = λx y. pu (papp x y) = λx y. papp x y

so,

λf g. (papp ** pu) (f, g) =
    λf g. (λ(a, b) (x, y). (a x, b y)) (f, g) =
    λf g (x, y). (f x, g y)

that is, pair_map_1 = pc (papp ** pu) = λf g (x, y). (f x, g y) and, we can read the type off from that last equation as (α → β) → (γ → δ) → α * γ → β * δ.

Now for $pair\_map_{2}$. We have

pc (papp ** papp ** pu) =
    (λk f g. k (f, g)) (papp ** papp ** pu) =
    λf g. (papp ** papp ** pu) (f, g)

where,

papp ** papp ** pu = papp ** (papp ** pu) =
    papp ** (λa' b'. pu (papp a' b')) =
    papp ** (λa' b'. papp a' b') = 
    λa b. (λa' b'. papp a' b') (papp a b)

which means,

pc (papp ** papp ** pu) = 
    λf g. (papp ** papp ** pu) (f, g) =
    λf g. (λa b.(λa' b'. papp a' b') (papp a b)) (f, g) =
    λf g. (λb. (λa' b'. papp a' b') (papp (f, g) b)) =
    λf g. λ(x, y). λa' b'. (papp a' b') (papp (f, g) (x, y)) =
    λf g. λ(x, y). λa' b'. (papp a' b') (f x, g y) =
    λf g. λ(x, y). λb'. papp (f x, g y) b' =
    λf g. λ(x, y). λ(x', y'). papp (f x, g y) (x', y') =
    λf g (x, y) (x', y'). (f x x', g y y')

that is, a function in two binary functions and two pairs as we expect. Phew! The type in this instance is (α → β → γ) → (δ → ε → ζ) → α * δ → β * ε → γ * ζ.

To finish off, here's the program transliterated into C++(14).

#include <utility>
#include <iostream>

//let pu x = x
auto pu = [](auto x) { return x; };

//let ( ** ) app k  = fun x y -> k (app x y)
template <class F, class K>
auto operator ^ (F app, K k) {
  return [=](auto x) {
    return [=] (auto y) {
      return k ((app (x)) (y));
    };
  };
}

//let pc k a b = k (a, b)
auto pc = [](auto k) {
  return [=](auto a) {
    return [=](auto b) { 
      return k (std::make_pair (a, b)); };
  };
};

//let papp (f, g) (x, y) = (f x, g y)
auto papp = [](auto f) { 
  return [=](auto x) { 
    return std::make_pair (f.first (x.first), f.second (x.second)); };
};

int main () {

  auto pair = &std::make_pair<int, int>;

  {
  auto succ= [](int x){ return x + 1; };
  auto pred= [](int x){ return x - 1; };
  auto p  = (pc (papp ^ pu)) (succ) (pred) (pair (1, 2));
  std::cout << p.first << ", " << p.second << std::endl;
  }

  {
  auto add = [](int x) { return [=](int y) { return x + y; }; };
  auto sub = [](int x) { return [=](int y) { return x - y; }; };
  auto p = pc (papp ^ papp ^ pu) (add) (sub) (pair(1, 2)) (pair (3, 4));
  std::cout << p.first << ", " << p.second << std::endl;
  }

  return 0;
}

REPLs

Reusable interactive REPL

I play around with little languages enough that I've found it useful to have a minimal language independent REPL for use as a library component. It is expressed as a single higher order function satisfying this signature:

val repl
    (eval : α list -> β -> γ)
    (pe : δ -> Lexing.lexbuf -> β)
    (tok : δ)
    (string_of_t : γ -> ε) : unit

The first argument eval is a function to evaluate expressions in the language, the second argument pe the parser entry point, tok is the lexer start token and the last argument string_of_t is a function that can compute a string from the result of an evaluated expression.

Here's an example session with a concrete repl for a basic $\lambda$ calculus interpreter (more on that later in this post):

  d:\lambda>.\lambda.exe
  ? (\p x y.p x y) (\x y. x) a b
  a
  ? (\p x y.p x y) (\x y. y) a b
  b

The driver for this program ('lambda_repl.ml') is as simple as this:

let main = 
  Repl.repl
    Lambda.eval
    Lambda_parser.main 
    Lambda_lexer.token
    Lambda.string_of_t

The module Repl follows ('repl.ml').

let parse 
    (pe : α -> Lexing.lexbuf -> β) 
    (le : α)
    (lexbuf : Lexing.lexbuf)  : β =
  try 
    pe le lexbuf
  with 
  | Parsing.Parse_error ->
    begin
      let curr = lexbuf.Lexing.lex_curr_p in
      let line = curr.Lexing.pos_lnum in
      let cnum = curr.Lexing.pos_cnum - curr.Lexing.pos_bol in
      let tok = Lexing.lexeme lexbuf in
      raise 
       (Failure (
          Printf.sprintf 
"file \"\", line %d, character %d\nError : Syntax error \"%s\"" 
            line cnum tok))
    end

let from_bytes ?(file : string = "") (str : string) 
    (pe : α -> Lexing.lexbuf -> β) 
    (le : α) : β =
  let set_filename lexbuf name =
    let open Lexing in
    lexbuf.lex_curr_p <-  {
      lexbuf.lex_curr_p with pos_fname = name
    } in
  let lexbuf = Lexing.from_string str in
  set_filename lexbuf file ;
  parse pe le lexbuf

let prompt (continuing:bool) =
  (print_string (if (not continuing)
    then "? " else "... ");(flush stdout))
let read (continuing:bool)=prompt continuing; input_line stdin

let handle_interpreter_error ?(finally=(fun () -> ())) ex =
  match ex with
  | Failure s -> finally () ; (Printf.printf "%s\n" s)
  | Stack_overflow -> finally () ; Printf.printf "Stack overflow\n"
  | Division_by_zero -> finally () ; Printf.printf "Division by zero\n"
  | End_of_file -> finally (); raise ex
  | _  as e -> 
    finally (); 
    Printf.printf "Unknown exception : %s\n" (Printexc.to_string e); 
    raise e

let safe_proc ?finally f =
  try f ()
  with exn -> handle_interpreter_error ?finally exn

let reduce 
    (eval : α list -> β -> γ)
    (pe : δ -> Lexing.lexbuf -> β)
    (le : δ)
    (to_bytes : γ -> ε) 
    (buf : Buffer.t) : ε =
  let t = 
    eval [] (from_bytes (Buffer.contents buf) pe le) in
  to_bytes t

let repl
    (eval : α list -> β -> γ)
    (pe : δ -> Lexing.lexbuf -> β)
    (tok : δ)
    (to_bytes : γ -> ε) : unit = 
  let initial_capacity = 4*1024 in
  let buf = Buffer.create initial_capacity in
  try 
    while true do
      let f () =
        let l = read ((Buffer.length buf)!=0) in
        let len = String.length l in
        if len > 0 then
          if l.[0] = '%' then ()
          else
            if l.[len - 1] = '\\' then
              (Buffer.add_string buf ((String.sub l 0 (len-1))^"\n"))
            else
              if l.[len-1] = (char_of_int 7) then Buffer.clear buf
              else
                let _ = Buffer.add_string buf l in
                let s = reduce eval pe tok to_bytes buf in
                Buffer.clear buf; print_endline s
      in (safe_proc ~finally:(fun () -> Buffer.clear buf) f)
    done
  with
  | End_of_file -> print_string "\n"

$\lambda$ calculus interpreter

This implementation is based on the techniques explained in Garrigue's excellent article "Code reuse through polymorphic variants".

First, a module implementing the simple language of variables ('var.ml').

type α impl = [`Var of string]
type t = α impl as α

let mk_var : string -> [> `Var of string] = fun s -> `Var s

let string_of_impl (_ : α -> string) : α impl -> string = function 
  | `Var s -> s

let rec string_of_t : t -> string = fun v -> string_of_impl string_of_t v

let eval_impl
    (env : (string * ([> `Var of string ] as α)) list) 
    (`Var s as v : α impl) : α =
  try
    List.assoc s env
  with
  | Not_found -> v

Next, a module extending this base language to implement the language of $\lambda$ expressions ('lambda.ml').

type α impl = [α Var.impl | `Abs of string * α | `App of α * α]
type t = α impl as α

let mk_app : α * β -> [> `App of α * β] = 
  fun (u, v) -> `App (u, v)
let mk_abs : string * β -> [> `Abs of string * β] = 
  fun (s, t) -> `Abs (s, t) 

module Detail = struct
  let gen_sym =
    let n = ref 0 in
    fun () -> incr n; "_" ^ string_of_int !n

  let rec strip (bs : string list) t =
    match t with 
    | `Abs (b, t) -> strip (b :: bs) t
    | _ as u -> (List.rev bs, u)

end (*module Detail*)

let string_of_impl (string_of_rec : α -> string) : α impl -> string = 
  function
  | #Var.t as v -> Var.string_of_impl string_of_rec v
  | `App (u, v) -> 
    "("^(string_of_rec u) ^ ") (" ^ (string_of_rec v)^")"
  | `Abs _ as t -> 
    match (Detail.strip [] t) with
    | (b :: bs, u)  ->
      let binder = 
        "\\" ^ b ^ (List.fold_right  (fun z b -> " " ^ z ^ b) bs ". ") in
      binder ^ (string_of_rec u)
    | ([], _) -> assert false

let rec string_of_t : t -> string = fun v -> string_of_impl string_of_t v

let eval_impl eval_rec 
    (env : (string *
              ([> 
                 `Abs of string * α 
               | `App of α * α 
               | `Var of string ] as α))
       list) : α impl -> α = function
    | #Var.t as v -> Var.eval_impl env v
    | `App (u, v) ->
      let v' = eval_rec env v in
      begin match eval_rec env u with
      | `Abs (s, body) -> eval_rec [s, v'] body
      | u' -> `App (u', v')
      end
    | `Abs (s, u) ->
      let s' = Detail.gen_sym () in
      `Abs (s', eval_rec ((s, `Var s') :: env) u)

let rec eval (env : (string * t) list) : t -> t = 
  eval_impl eval env

That's it for the interpreter. All that remains is to put a "front end" on it. First the parser ('lambda_parser.mly').

%{
type t = Lambda.t

let var (s : string) : t = 
  Var.mk_var s

let abs ((bs : string list), (t : t)) : t =
  List.fold_right (fun b u -> Lambda.mk_abs (b, u)) bs t
let app ((t0 : t), (us : t list)) : t =
  List.fold_left (fun t u -> Lambda.mk_app (t, u)) t0 us

%}
 
%token  Tident
%token  Tnum
%token Tlambda Tdot Tlparen Trparen Teof

%nonassoc Tident Tdot Tlparen Trparen Teof

%start main
%type  main

%%
main:
  | term Teof { $1 }
  ;
term:
  | Tlambda id id_list Tdot term { abs (($2 :: $3), $5) }
  | atom atom_list { app ($1, $2) }
  ;
atom_list:
  | { [] }
  | atom atom_list { $1 :: $2 }
  ;
atom:
  | id { var $1 }
  | Tlparen term Trparen { $2 }
  ;
id_list:
  | { [] }
  | id id_list { $1 :: $2 }
  ;
id:
  | Tident { $1 }
  ;
%%

Lastly, the lexical analyzer ('lambda_lexer.mll').

{
  open Lambda_parser
}

let alpha=['a'-'z' 'A'-'Z']

rule token = parse
    ['\r' ' ' '\t' '\n']              { token lexbuf }
  | '('                                    { Tlparen }
  | ')'                                    { Trparen }
  | '\\'                                   { Tlambda }
  | '.'                                       { Tdot }
  | ((alpha)(alpha)*) as s                { Tident s }
  | eof                                       { Teof }

Church Numerals

This is just a little fun. Jason Hickey in "Introduction to Objective Caml" poses some little end of chapter problems to define arithmetic operations for a type of unary (base-1) natural numbers. The type is

type num = Z | S of num

where Z represents the number zero and if i is a unary number, then S i is i + 1.

This formulation of Church numerals using a recursive type and pattern matching means in truth, the problems can be solved in less than 5 minutes or so. Of course, the real Church numerals are numbers encoded in functions

• $c_{0} = \lambda s.\lambda z.\;z$
• $c_{1} = \lambda s.\lambda z.\;s\;z$
• $c_{2} = \lambda s.\lambda z.\;s\;(s\;z)$
• $c_{3} = \lambda s.\lambda z.\;s\;(s\;(s\;z))$
• $\cdots$

and their represenation including arithmetic operations can be formulated in OCaml too (and it's a good exercise but harder than what we are going to do here -- if you'd like to see more about that, have a look at this Cornell lecture).

Alright, without further ado, here we go then.

type num = Z | S of num

let scc (x : num) : num = S x
let prd : num -> num = function | S n -> n | _ -> Z

let rec add (x : num) (y : num) : num =
  match (x, y) with 
  | (Z, _) -> y
  | (_, Z) -> x
  | (S m, n) -> scc (add m n)

let rec sub (x : num) (y : num) : num =
  match (x, y) with
  | (Z, _) -> Z
  | (n, Z) -> n
  | (S m, n) -> sub m (prd n)

let rec mul (x : num) (y : num) : num = 
  match (x, y) with
  | (Z, _) -> Z
  | (_, Z) -> Z
  | (S Z, x) -> x
  | (x, S Z) -> x
  | (S m, n) -> add (mul m n) n

let rec to_int : num -> int = function | Z -> 0 | S n -> 1 + to_int n
let rec from_int (x : int)  = if x = 0 then Z else scc (from_int (x - 1))

For example, in the top-level we can write things like,

# to_int (mul (sub (from_int 23) (from_int 11)) (from_int 2));;
- : int = 24

The main thing I find fun about this little program though is how obvious its mapping to C++. Of course you need a discriminated union type my default choice being boost::variant<> (by the way, standardization of a variant type for C++ is very much under active discussion and development, see N4450 for example from April this year - it seems that support for building recursive types might not be explicitly provided though... That would be a shame in my opinion and if that's the case, I beg the relevant parties to reconsider!).

#include <boost/variant.hpp>
#include <boost/variant/apply_visitor.hpp>

#include <stdexcept>
#include <iostream>

struct Z;
struct S;

typedef boost::variant<Z, boost::recursive_wrapper<S>> num;

struct Z {};
struct S { num i; };

int to_int (num const& i);

struct to_int_visitor 
  : boost::static_visitor<int> {
  int operator ()(Z const& n) const { return 0; }
  int operator ()(S const& n) const { return 1 + to_int (n.i); }
};

int to_int (num const& i) {
  return boost::apply_visitor (to_int_visitor (), i);
}

num from_int (int i) {
  if (i == 0){
    return Z {};
  }
  else{
    return S {from_int (i - 1)};
  }
}

num add (num l, num r);

struct add_visitor : boost::static_visitor<num> {
  num operator () (Z, S s) const { return s; }
  num operator () (S s, Z) const { return s; }
  num operator () (Z, Z) const { return Z {}; }
  num operator () (S s, S t) const { return S { add (s.i, t) }; }
};

num add (num l, num r) {
  return boost::apply_visitor (add_visitor (), l, r);
}

num succ (num x) { return S{x}; }

struct prd_visitor : boost::static_visitor<num>{
  num operator () (Z z) const { return z; }
  num operator () (S s) const { return s.i; }
};

num prd (num x) {
  return boost::apply_visitor(prd_visitor (), x);
}

num sub (num x, num y);

struct sub_visitor : boost::static_visitor<num> {
  num operator () (Z, Z) const { return Z {}; }
  num operator () (Z, S) const { return Z {}; }
  num operator () (S m, Z) const { return m; }
  num operator () (S m, S n) const { return sub (m.i, prd (n)); }
};

num sub (num x, num y) {
  return boost::apply_visitor (sub_visitor (), x, y);
}

//Tests

int main () {

  num zero = Z {};
  num one = succ (zero);
  num two = succ (succ (zero));
  num three = succ (succ (succ (zero)));

  std::cout << to_int (add (two, three)) << std::endl;
  std::cout << to_int (sub (from_int (23), from_int (12))) << std::endl;

  return 0;
}

I didn't get around to implementing mul in the above. Consider it an "exercise for the reader"!

Y Combinator

There is this blog post by Caltech computer scientist, Mike Vanier. The code in Mike's article uses the Scheme programming language. This one uses Python.

A $Y$ combinator is a higher-order function which, given argument $f$ (say,) satisfies the equation $Y f = f\;(Y f)$. They are said to compute a "fixed point" $f^{'}$ of their argument $f$ since $f^{'} = Y\;f = f\;(Y\;f) = f \;f^{'}$.

A $Y$ combinator takes a function that isn't recursive and returns a version of the function that is. That is, $Y$ is a function that takes $f$ and returns $f (f (f (\cdots)))$.

The existence of $Y$ combinators is amazing in that it tells us that it is possible to write recursive functions even in a programming language that says nothing about recursion!

The goal here is to derive a $Y$.

Start with the classic recursive definition of the factorial function.

  def fact (n) :
    if n == 0 : 
      return 1 
    else: 
      return n * fact (n - 1)

We are trying to eliminate explicit recursion. To that end, factor out the recursive call and make it an application of a function argument.

def part_fact (this, n):
  if n == 0 :
    return 1
   else:
     return n * this (this, (n - 1))

fact = functools.partial(part_fact, part_fact)

That's sufficient to get rid of the explicit recursion but we mean to push on in search of a "library" solution to this problem, that is, some general result that can be re-used.

Next let's get this down to a function in one argument as is this way in the $\lambda$ calculus.

  def part_fact (this):
    return lambda n : 1 if n == 0 else n * (this (this)) (n - 1)

  fact = part_fact (part_fact)

We'd recover something tantalizingly close to the original factorial function if we factored out this (this) into a function of one argument.

def part_fact (this):
  f = this (this)
  return lambda n : 1 if n == 0 else n * f (n - 1)
fact = part_fact(part_fact)

This would be fine in a lazy language but Python is a strict language and exhibits infinite recursion because to evaluate part_fact (part_fact) requires evaluating f = part_fact (part_fact) and so on. The solution is to delay the evaluation until it's needed.

def part_fact (this):
  f = lambda y : (this (this)) y
  return lambda n : 1 if n == 0 else n * f (n - 1)
fact = part_fact(part_fact)

Refactor this into two parts.

def almost_fact (f):
  return lambda n : 1 if n == 0 else f (n - 1)

def part_fact (this):
  f = lambda y : (this (this))(y)
  return almost_fact (f)

fact = part_fact(part_fact)

Rephrase part_frac as a lambda and change the argument name to x.

def almost_fact (f):
  return lambda n : 1 if n == 0 else f (n - 1)

part_fract = lambda x : almost_fact (lambda y : (x (x))(y))

fact = part_fact (part_fact)

Eliminate 'part_fact'.

def almost_fact (f):
  return lambda n : 1 if n == 0 else f (n - 1)

fact = (lambda x : almost_fact (lambda y : (x (x))(y))) \
          (lambda x : almost_fact (lambda y : (x (x))(y)))

That's it! There's the $Y$ combinator. Generalize.

def Y (f):
 return (lambda x : f (lambda y : (x (x))(y))) \
           (lambda x : f (lambda y : (x (x))(y)))

def almost_fact (f):
  return lambda n : 1 if n == 0 else f (n - 1)

fact = Y (almost_fact)

That is, $Y = \lambda f.(\lambda x. f\;(\lambda y. (x\;x)\;y))\;(\lambda x. f\;(\lambda y. (x\;x)\;y))$. This $Y$ combinator is known s Curry's paradoxical combinator (in its "applicative order" form to account for the fact that Python is strict).

Try this on another function. Fibonacci numbers say.

def almost_fib (f) :
  return lambda n : 1 if n <= 2 else f (n - 1) + f (n - 2)

fib = Y (almost_fib)

print (str (fib (6))+"\n") #Prints '8'