[go: nahoru, domu]
Skip to content

Instantly share code, notes, and snippets.

@travisallison

travisallison/CoC.ml

Forked from hirrolot/CoC.ml
Created December 28, 2023 21:31
Show Gist options
  • Save travisallison/b85b9a43419f8e9cb84f1e06be85e3db to your computer and use it in GitHub Desktop.
Save travisallison/b85b9a43419f8e9cb84f1e06be85e3db to your computer and use it in GitHub Desktop.
Download ZIP
Barebones lambda cube in OCaml
Raw
a-preface.md

Barebones lambda cube in OCaml

For any formal system, we can really only understand its precise details after attempting to implement it.
    -- Simon Thompson, Type Theory & Functional Programming 1

This post has been discussed on Reddit.

This post has a followup.

Since a type theory called "Calculus of Constructions (CoC)" was introduced by Thierry Coquand in 1985, its conceptual elegance has been a subject of interest to many enlightened mathematicians and computer scientists. Since then, its extended variants have found their use in proof assistants, such as Lean and Coq, and programming languages as well, such as Neut, Agda, Idris, and many others. For a logician, CoC can be used as a foundation of (constructive) mathematics; for a programmer, it can be seen as a basis of a programming language whose types correspond to logical propositions, thus making theorem proving and software development proceed within a single system.

The lambda cube is a formal system introduced by Henk Barendregt, that depicts the directions of how simply typed lambda calculus can be extended to form different combinations of terms and types depending on each other (i.e., function types). Thus, vertices in the cube correspond to specific type theories, and the most expressive vertex is CoC itself since it permits all the combinations of terms and types as input and output values:

(Adapted from Wikipedia.)

In the context of programming, this observation sums up the four base paradigms of structuring code:

Combination Paradigm
Terms depending on terms Algorithms and data structures.
Terms depending on types Generic programming.
Types depending on types Type-level programming; metaprogramming.
Types depending on terms Dependent typing; formal verification.

Although CoC is a simple system, it is not straightforward to implement it on a computer: you need to guarantee capture-free substitution, alpha equivalence of terms, uniqueness of types up to beta conversion, and other peculiarities. For this reason, I wrote a minimalistic implementation of CoC in OCaml so that other learners of type theory could benefit from it. You will not see a parser, enhanced diagnostics, or any type system extensions -- everything you will see is just an abstract syntax representation, poor man's type inference, and beta reduction.

As an application of the developed system, I present the encoding of Church booleans, Church numerals, intuitionistic logic, and classical logic with the law of double negation. Finally, I provide unit tests for (almost) all functions involved in the implementation. The characteristics of the implementation are typing à la Church (explicitly typed binders), applicative order evaluation (arguments evaluated first), and a named representation of variables.

All the material presented here should be accessible after reading the first seven chapters from "Type Theory and Formal Proof: An Introduction". Other remarkable literature is included 2 3 4 5.

See also: untyped lambda calculus on the C preprocessor.

Show unit tests 
let test_free_vars () =
  assert (free_vars (Var "x") = [ "x" ]);
  assert (free_vars (lam "x" Star (Var "x")) = []);
  assert (free_vars (lam "x" (Var "y") (Var "x")) = [ "y" ]);
  assert (free_vars (lam "x" Star (Var "y")) = [ "y" ]);
  assert (free_vars (lam "x" (Var "x") (Var "y")) = [ "x"; "y" ]);
  assert (free_vars (Appl (Var "x", Var "y")) = [ "x"; "y" ]);
  assert (free_vars Star = []);
  assert (free_vars Box = [])

let test_binders () =
  assert (binders (Var "x") = []);
  assert (binders (lam "x" Star (Var "x")) = [ "x" ]);
  assert (binders (lam "x" (Var "y") (Var "x")) = [ "x" ]);
  assert (binders (lam "x" Star (Var "y")) = [ "x" ]);
  assert (binders (lam "x" (pi "y" Star (Var "y")) (Var "x")) = [ "x"; "y" ]);
  assert (binders (Appl (Var "x", Var "y")) = []);
  assert (
    binders (Appl (lam "x" Star (Var "z"), lam "y" Star (Var "z")))
    = [ "x"; "y" ]);
  assert (binders Star = []);
  assert (binders Box = [])

let test_fresh_var () =
  assert (freshen [] "x" = "x");
  assert (freshen [ "x" ] "y" = "y");
  assert (freshen [ "x" ] "x" = "x'");
  assert (freshen [ "x"; "x'"; "x''"; "y"; "z" ] "x" = "x'''")

let test_subst () =
  assert (subst "x" (Var "y") (Var "x") = Var "y");
  assert (subst "y" (Var "z") (Var "x") = Var "x");
  assert (subst "x" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "z", Var "y"));
  assert (subst "y" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "x", Var "z"));
  assert (subst "x" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "z", Var "y"));
  assert (subst "z" (Var "l") (Appl (Var "x", Var "y")) = Appl (Var "x", Var "y"));
  assert (subst "x" (Var "z") (lam "x" Star (Var "x")) = lam "x" Star (Var "x"));
  assert (
    subst "x" (Var "z") (lam "x" (Var "x") (Var "x"))
    = lam "x" (Var "z") (Var "x"));
  assert (subst "y" (Var "z") (lam "x" Star (Var "y")) = lam "x" Star (Var "z"));
  (* Check that the new binding variable does not accidentally capture the
     substitution term... *)
  assert (subst "y" (Var "x") (lam "x" Star (Var "y")) = lam "x'" Star (Var "x"));
  (* ... and that it does not capture free variables in the body. *)
  assert (
    subst "y" (Var "x") (lam "x" Star (Appl (Var "y", Var "x'")))
    = lam "x''" Star (Appl (Var "x", Var "x'")));
  (* ... and that it does not conflict with bindings in the body. *)
  assert (
    subst "y" (Var "x") (lam "x" Star (lam "x'" Star (Appl (Var "y", Var "x"))))
    = lam "x''" Star (lam "x'" Star (Appl (Var "x", Var "x''"))));
  assert (subst "x" (Var "z") Star = Star);
  assert (subst "x" (Var "z") Box = Box)

let test_alpha_eq () =
  assert (alpha_eq (Var "x", Var "x"));
  assert (not (alpha_eq (Var "x", Var "y")));
  assert (alpha_eq (Appl (Var "x", Var "y"), Appl (Var "x", Var "y")));
  assert (not (alpha_eq (Appl (Var "x", Var "z"), Appl (Var "x", Var "y"))));
  assert (not (alpha_eq (Appl (Var "z", Var "y"), Appl (Var "x", Var "y"))));
  assert (alpha_eq (lam "x" Star (Var "x"), lam "x" Star (Var "x")));
  assert (alpha_eq (lam "x" Star (Var "x"), lam "y" Star (Var "y")));
  assert (not (alpha_eq (lam "x" Star (Var "x"), lam "y" (Var "z") (Var "y"))));
  assert (alpha_eq (pi "x" Star (Var "x"), pi "x" Star (Var "x")));
  assert (alpha_eq (pi "x" Star (Var "x"), pi "y" Star (Var "y")));
  assert (not (alpha_eq (pi "x" Star (Var "x"), pi "y" (Var "z") (Var "y"))))

let test_eval () =
  assert (eval (Var "x") = Var "x");
  assert (eval (Appl (Var "x", Var "y")) = Appl (Var "x", Var "y"));
  assert (eval (Appl (lam "x" (Var "a") (Var "x"), Var "y")) = Var "y");
  (* If `m` in `Appl(m, n)` is not an immediate lambda, we must first normalise
     it and see if it is. *)
  assert (
    eval
      (Appl
         ( Appl (lam "x" (Var "a") (lam "x" (Var "a") (Var "x")), Var "z"),
           Var "y" ))
    = Var "y");
  (* If `m` in `Appl(m, n)` is not a redex, we must nonetheless evaluate `n` and
     return the application. *)
  assert (
    eval (Appl (Var "x", Appl (lam "x" (Var "a") (Var "x"), Var "y")))
    = Appl (Var "x", Var "y"));
  (* Check that an argument is evaluated. *)
  assert (
    eval
      (Appl
         ( lam "x" (Var "a") (Var "x"),
           Appl (lam "x" (Var "a") (Var "x"), Var "z") ))
    = Var "z");
  (* Check that a body after substitution is evaluated. *)
  assert (
    eval
      (Appl
         ( lam "x" (Var "a") (Appl (lam "y" (Var "a") (Var "y"), Var "x")),
           Var "z" ))
    = Var "z");
  assert (eval (lam "x" (Var "a") (Var "x")) = lam "x" (Var "a") (Var "x"));
  (* Both an argument type and a body must be evaluated. *)
  assert (
    eval
      (lam "x"
         (Appl (lam "x" (Var "a") (Var "x"), Var "y"))
         (Appl (lam "x" (Var "a") (Var "x"), Var "z")))
    = lam "x" (Var "y") (Var "z"));
  assert (eval Star = Star);
  assert (eval Box = Box)

let test_type_inference () =
  (* Super-type "*". *)
  assert (infer_type Star = Box);
  assert (infer_type ~ctx:[ ("x", Star); ("y", Var "x") ] Star = Box);
  (* Variables. *)
  assert (infer_type ~ctx:[ ("x", Star) ] (Var "x") = Star);
  assert (
    infer_type ~ctx:[ ("x", Star); ("y", Var "x"); ("z", Var "x") ] (Var "y")
    = Var "x");
  assert (infer_type ~ctx:[ ("x", Star); ("y", Var "x") ] (Var "y") = Var "x");
  (* Application. *)
  assert (
    infer_type
      ~ctx:[ ("a", Star); ("y", Var "a") ]
      (Appl (lam "x" (Var "a") (Var "x"), Var "y"))
    = Var "a");
  assert (
    infer_type ~ctx:[ ("y", Star) ] (Appl (lam "x" Star (Var "x"), Var "y"))
    = Star);
  (* A term depending on a term. *)
  assert (
    infer_type ~ctx:[ ("a", Star) ] (lam "x" (Var "a") (Var "x"))
    = pi "x" (Var "a") (Var "a"));
  (* A term depending on a type. *)
  assert (
    infer_type ~ctx:[ ("a", Star); ("y", Var "a") ] (lam "x" Star (Var "y"))
    = pi "x" Star (Var "a"));
  (* A type depending on a type. *)
  assert (infer_type (lam "x" Star (Var "x")) = pi "x" Star Star);
  (* A type depending on a term. *)
  assert (
    infer_type ~ctx:[ ("a", Star) ] (lam "x" (Var "a") (Var "a"))
    = pi "x" (Var "a") Star);
  assert (
    infer_type
      ~ctx:[ ("a", Star) ]
      (lam "x" (Var "a") (pi "y" (Var "a") (Var "a")))
    = pi "x" (Var "a") Star);
  (* Pi-types. *)
  assert (infer_type ~ctx:[ ("a", Star) ] (pi "x" (Var "a") (Var "a")) = Star);
  assert (
    infer_type
      ~ctx:[ ("a", Star) ]
      (pi "x" (Var "a") (pi "x" (Var "a") (Var "a")))
    = Star);
  assert (infer_type ~ctx:[ ("a", Box) ] (pi "x" (Var "a") (Var "a")) = Box);
  assert (
    infer_type
      ~ctx:[ ("a", Box) ]
      (pi "x" (Var "a") (pi "x" (Var "a") (Var "a")))
    = Box);
  (* Our evaluator must normalise all subexpressions. *)
  assert (
    infer_type
      ~ctx:[ ("a", Star); ("b", Star); ("y", Var "a"); ("z", Var "b") ]
      (lam "x"
         (Appl (lam "x" Star (Var "x"), Var "a"))
         (Appl (lam "x" (Var "b") (Var "x"), Var "z")))
    = pi "x" (Var "a") (Var "b"))

let test_print () =
  assert (print (Var "x") = "x");
  assert (print (Appl (Var "x", Var "y")) = "(x y)");
  assert (print (lam "x" (Var "z") (Var "x")) = "(λx:z.x)");
  assert (print (pi "x" Star (Var "x")) = "(Πx:*.x)");
  assert (print (pi "x" (Var "a") (Var "a")) = "(a→a)");
  assert (print (pi "a" Star (pi "x" (Var "a") (Var "a"))) = "(Πa:*.(a→a))");
  assert (print Star = "*");
  assert (print Box = "☐")

let () =
  test_free_vars ();
  test_binders ();
  test_fresh_var ();
  test_subst ();
  test_alpha_eq ();
  test_eval ();
  test_type_inference ();
  test_print ()

Footnotes

  1. https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ↩

  2. https://github.com/steshaw/plt ↩

  3. https://github.com/jozefg/learn-tt ↩

  4. https://proofassistants.stackexchange.com/questions/930/so-many-data-types-so-little-time/940#940 ↩

  5. http://lucacardelli.name/Papers/TypeSystems.pdf ↩

Raw
CoC.ml
(* The syntax of our calculus. Notice that types are represented in the same way
as terms, which is the essence of CoC. *)
type term =
| Var of string
| Appl of term * term
| Binder of binder * string * term * term
| Star
| Box
and binder = Lam | Pi
let lam x a m = Binder (Lam, x, a, m)
let pi x a m = Binder (Pi, x, a, m)
let rec free_vars = function
| Var x -> [ x ]
| Appl (m, n) -> free_vars m @ free_vars n
| Binder (_, x, a, m) -> free_vars a @ List.filter (( <> ) x) (free_vars m)
| Star | Box -> []
let rec binders = function
| Appl (m, n) -> binders m @ binders n
| Binder (_, x, a, m) -> [ x ] @ binders a @ binders m
| Var _ | Star | Box -> []
let all_vars t = free_vars t @ binders t
(* Generates a fresh variable identifier that is not in a banlist. *)
let rec freshen (banlist : string list) (base : string) =
if List.mem base banlist then freshen banlist (base ^ "'") else base
let rec print = function
| Var x -> x
| Appl (m, n) -> Printf.sprintf "(%s %s)" (print m) (print n)
| Binder (Lam, x, a, m) -> Printf.sprintf "(λ%s:%s.%s)" x (print a) (print m)
| Binder (Pi, x, a, m) ->
if List.mem x (free_vars m) then
Printf.sprintf "(Π%s:%s.%s)" x (print a) (print m)
else Printf.sprintf "(%s→%s)" (print a) (print m)
| Star -> "*"
| Box -> "☐"
let rec subst x m = function
| Var y when x = y -> m
| Var y -> Var y
| Appl (m', n) -> Appl (subst x m m', subst x m n)
| Binder (binder, y, a, n) when x = y -> Binder (binder, y, subst x m a, n)
| Binder (binder, y, a, n) when List.mem y (free_vars m) ->
let banlist = free_vars m @ all_vars n in
subst x m (rename (freshen banlist y) (binder, y, a, n))
| Binder (binder, y, a, n) -> Binder (binder, y, subst x m a, subst x m n)
| (Star | Box) as s -> s
and rename x' (binder, x, a, m) = Binder (binder, x', a, subst x (Var x') m)
(* With De Bruijn indices, alpha equivalence check amounts to structural
equality. However, we use named representation because it is more convenient
for the user interface. *)
let rec alpha_eq = function
| Var x, Var x' -> x = x'
| Appl (m, n), Appl (m', n') -> alpha_eq (m, m') && alpha_eq (n, n')
| Binder (binder, x, a, m), Binder (binder', x', a', m') when x = x' ->
binder = binder' && alpha_eq (a, a') && alpha_eq (m, m')
| Binder (binder, x, a, m), Binder (binder', x', a', m') ->
let banlist = all_vars m @ all_vars m' in
let fresh_x = freshen banlist x in
alpha_eq
(rename fresh_x (binder, x, a, m), rename fresh_x (binder', x', a', m'))
| Star, Star | Box, Box -> true
| _, _ -> false
let panic fmt = Printf.ksprintf failwith fmt
(* Reduces a term to its beta normal form using applicative order. *)
let rec eval = function
| Appl (m, n) -> eval_appl (eval m) (eval n)
| Binder (binder, x, a, m) -> Binder (binder, x, eval a, eval m)
| (Var _ | Star | Box) as t -> t
and eval_appl m n =
match m with Binder (Lam, x, _a, m) -> eval (subst x n m) | _ -> Appl (m, n)
(* A list of variable declarations for type inference. *)
type context = (string * term) list
(* Infers a type, in beta normal form, of a term in a given (well-formed)
context; throws an exception otherwise. *)
let rec infer_type ?(ctx : context = []) = function
| Var x -> eval (List.assoc x ctx)
| Appl (m, n) -> infer_appl ctx m n
| Binder (Lam, x, a, m) ->
let m_ty = infer_type ~ctx:((x, a) :: ctx) m in
let lam_ty = Binder (Pi, x, a, m_ty) in
(* Check that the lambda type we have inferred is well-formed. *)
let _ = infer_type ~ctx lam_ty in
eval lam_ty
| Binder (Pi, x, a, m) ->
let _s1 = infer_sort ctx a in
let s2 = infer_sort ((x, a) :: ctx) m in
s2
| Star -> Box
| Box -> panic "☐ has no type"
and infer_appl (ctx : context) m n =
match infer_type ~ctx m with
| Binder (Pi, x, a, m) ->
let n_ty = infer_type ~ctx n in
if alpha_eq (a, n_ty) then eval (subst x n m)
else panic "Expected type %s, got %s: %s" (print a) (print n_ty) (print n)
| m_ty ->
panic "Application of argument %s to a non-lambda %s of type %s" (print n)
(print m) (print m_ty)
and infer_sort (ctx : context) t =
match infer_type ~ctx t with
| (Star | Box) as s -> s
| a -> panic "Expected a sort, got %s: %s" (print a) (print t)
let check_type ?(ctx : context = []) t expected_ty =
assert (alpha_eq (infer_type ~ctx t, eval expected_ty))
Raw
usage.ml
(* Define some syntax for variable arguments. Left/right folds over lists
beautifully mirror the left/right-associative nature of applications and
lambda abstractions, respectively. *)
let binder' binder ctx m =
match ctx with
| [] -> failwith "Empty argument list"
| ctx -> List.fold_right (fun (x, a) acc -> Binder (binder, x, a, acc)) ctx m
let lam' ctx m = binder' Lam ctx m
let pi' ctx m = binder' Pi ctx m
let appl = function
| [] -> failwith "Empty application list"
| t :: ts -> List.fold_left (fun m n -> Appl (m, n)) t ts
let check ?(ctx = []) t expected =
(* Check that the term is actually well-typed before evaluating. *)
let _ = infer_type ~ctx t in
assert (alpha_eq (eval t, eval expected))
let church_booleans () =
let t = lam' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "x") in
let f = lam' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "y") in
let bool_ty = pi' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "a") in
assert (infer_type t = bool_ty);
assert (infer_type f = bool_ty);
let if_then_else =
lam'
[ ("a", Star); ("b", bool_ty); ("x", Var "a"); ("y", Var "a") ]
(appl [ Var "b"; Var "a"; Var "x"; Var "y" ])
in
check
~ctx:[ ("a", Star); ("x", Var "a"); ("y", Var "a") ]
(appl [ if_then_else; Var "a"; t; Var "x"; Var "y" ])
(Var "x");
check
~ctx:[ ("a", Star); ("x", Var "a"); ("y", Var "a") ]
(appl [ if_then_else; Var "a"; f; Var "x"; Var "y" ])
(Var "y");
let my_not = lam "b" bool_ty (appl [ Var "b"; bool_ty; f; t ]) in
check (appl [ my_not; t ]) f;
check (appl [ my_not; f ]) t;
let my_and =
lam'
[ ("a", bool_ty); ("b", bool_ty) ]
(appl [ Var "a"; bool_ty; Var "b"; f ])
in
check (appl [ my_and; t; t ]) t;
check (appl [ my_and; t; f ]) f;
check (appl [ my_and; f; f ]) f;
check (appl [ my_and; f; t ]) f;
let my_or =
lam'
[ ("a", bool_ty); ("b", bool_ty) ]
(appl [ Var "a"; bool_ty; t; Var "b" ])
in
check (appl [ my_or; t; t ]) t;
check (appl [ my_or; t; f ]) t;
check (appl [ my_or; f; f ]) f;
check (appl [ my_or; f; t ]) t;
let my_xor =
lam'
[ ("a", bool_ty); ("b", bool_ty) ]
(appl [ Var "a"; bool_ty; appl [ my_not; Var "b" ]; Var "b" ])
in
check (appl [ my_xor; t; t ]) f;
check (appl [ my_xor; t; f ]) t;
check (appl [ my_xor; f; f ]) f;
check (appl [ my_xor; f; t ]) t
let church_numerals () =
let f_ty = pi "x" (Var "a") (Var "a") in
let n_ty = pi' [ ("a", Star); ("f", f_ty); ("x", Var "a") ] (Var "a") in
let zero = lam' [ ("a", Star); ("f", f_ty); ("x", Var "a") ] (Var "x") in
let succ =
lam'
[ ("n", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
(appl [ Var "f"; appl [ Var "n"; Var "a"; Var "f"; Var "x" ] ])
in
let [ succ; zero ] in
let two = appl [ succ; one ] in
let three = appl [ succ; two ] in
let four = appl [ succ; three ] in
assert (infer_type zero = n_ty);
assert (infer_type >
assert (infer_type two = n_ty);
assert (infer_type three = n_ty);
assert (infer_type four = n_ty);
let add =
lam'
[ ("n", n_ty); ("m", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
(appl
[
Var "n";
Var "a";
Var "f";
appl [ Var "m"; Var "a"; Var "f"; Var "x" ];
])
in
check (appl [ add; zero; zero ]) zero;
check (appl [ add; zero; one ]) one;
check (appl [ add; one; zero ]) one;
check (appl [ add; three; one ]) four;
let mul =
lam'
[ ("n", n_ty); ("m", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
(appl [ Var "n"; Var "a"; appl [ Var "m"; Var "a"; Var "f" ]; Var "x" ])
in
check (appl [ mul; zero; zero ]) zero;
check (appl [ mul; zero; one ]) zero;
check (appl [ mul; one; two ]) two;
check (appl [ mul; two; two ]) four
let intuitionistic_logic () =
(* A => (B => A) *)
check_type
(lam'
[ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
(Var "x"))
(pi' [ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ] (Var "a"));
let absurdity = pi "a" Star (Var "a") in
let negate = lam "a" Star (pi "x" (Var "a") absurdity) in
(* not A => (A => B) *)
check_type
(lam'
[ ("a", Star); ("b", Star); ("x", appl [ negate; Var "a" ]) ]
(lam "y" (Var "a") (appl [ Var "x"; Var "y"; Var "b" ])))
(pi'
[ ("a", Star); ("b", Star); ("x", appl [ negate; Var "a" ]) ]
(pi "y" (Var "a") (Var "b")));
(* A & B; product type *)
let conj =
lam'
[ ("a", Star); ("b", Star) ]
(pi'
[
("c", Star); ("x", pi' [ ("l", Var "a"); ("m", Var "b") ] (Var "c"));
]
(Var "c"))
in
let a_and_b_ty = appl [ conj; Var "a"; Var "b" ] in
let b_and_a_ty = appl [ conj; Var "b"; Var "a" ] in
(* A => B => A & B *)
let conj_intro =
lam'
[ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
(lam'
[
("c", Star); ("k", pi' [ ("l", Var "a"); ("m", Var "b") ] (Var "c"));
]
(appl [ Var "k"; Var "x"; Var "y" ]))
in
check_type conj_intro
(pi'
[ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
a_and_b_ty);
(* A & B => A *)
let conj_elim1 =
lam'
[ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
(appl
[ Var "x"; Var "a"; lam' [ ("l", Var "a"); ("m", Var "b") ] (Var "l") ])
in
check_type conj_elim1
(pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] (Var "a"));
(* A & B => B *)
(let conj_elim2 =
lam'
[ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
(appl
[
Var "x"; Var "b"; lam' [ ("l", Var "a"); ("m", Var "b") ] (Var "m");
])
in
check_type conj_elim2
(pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] (Var "b"));
(* A & B => B & A *)
check_type
(lam'
[ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
(appl
[
conj_intro;
Var "b";
Var "a";
appl [ conj_elim2; Var "a"; Var "b"; Var "x" ];
appl [ conj_elim1; Var "a"; Var "b"; Var "x" ];
]))
(pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] b_and_a_ty));
(* A | B; sum type *)
let disj =
lam'
[ ("a", Star); ("b", Star) ]
(pi'
[
("c", Star);
("x", pi "l" (Var "a") (Var "c"));
("y", pi "l" (Var "b") (Var "c"));
]
(Var "c"))
in
let a_or_b_ty = appl [ disj; Var "a"; Var "b" ] in
let b_or_a_ty = appl [ disj; Var "b"; Var "a" ] in
(* A => A | B *)
let disj_intro1 =
lam'
[ ("a", Star); ("b", Star); ("v", Var "a") ]
(lam'
[
("c", Star);
("x", pi "l" (Var "a") (Var "c"));
("y", pi "l" (Var "b") (Var "c"));
]
(appl [ Var "x"; Var "v" ]))
in
check_type disj_intro1
(pi' [ ("a", Star); ("b", Star); ("v", Var "a") ] a_or_b_ty);
(* B => A | B *)
let disj_intro2 =
lam'
[ ("a", Star); ("b", Star); ("v", Var "b") ]
(lam'
[
("c", Star);
("x", pi "l" (Var "a") (Var "c"));
("y", pi "l" (Var "b") (Var "c"));
]
(appl [ Var "y"; Var "v" ]))
in
check_type disj_intro2
(pi' [ ("a", Star); ("b", Star); ("v", Var "b") ] a_or_b_ty);
(* A | B => B | A *)
check_type
(lam'
[ ("a", Star); ("b", Star); ("x", a_or_b_ty) ]
(appl
[
Var "x";
b_or_a_ty;
lam "l" (Var "a") (appl [ disj_intro2; Var "b"; Var "a"; Var "l" ]);
lam "l" (Var "b") (appl [ disj_intro1; Var "b"; Var "a"; Var "l" ]);
]))
(pi' [ ("a", Star); ("b", Star); ("x", a_or_b_ty) ] b_or_a_ty);
let not_a_or_b = appl [ negate; appl [ disj; Var "a"; Var "b" ] ] in
let not_a_and_not_b =
appl [ conj; appl [ negate; Var "a" ]; appl [ negate; Var "b" ] ]
in
(* not (A | B) => (not A) & (not B) *)
check_type
(lam'
[ ("a", Star); ("b", Star); ("x", not_a_or_b) ]
(appl
[
conj_intro;
appl [ negate; Var "a" ];
appl [ negate; Var "b" ];
lam "y" (Var "a")
(appl
[ Var "x"; appl [ disj_intro1; Var "a"; Var "b"; Var "y" ] ]);
lam "y" (Var "b")
(appl
[ Var "x"; appl [ disj_intro2; Var "a"; Var "b"; Var "y" ] ]);
]))
(pi' [ ("a", Star); ("b", Star); ("x", not_a_or_b) ] not_a_and_not_b);
(* Universal quantification; dependent function type. *)
let forall =
lam'
[ ("a", Star); ("p", pi "x" (Var "a") Star) ]
(pi "x" (Var "a") (appl [ Var "p"; Var "x" ]))
in
(* We get the introduction and elimination rules for universal quantification
for free: they are just lambda abstraction and application. *)
(* Existential quantification; sigma type. *)
let exists =
lam'
[ ("a", Star); ("p", pi "x" (Var "a") Star) ]
(pi'
[
("c", Star);
( "f",
pi' [ ("x", Var "a"); ("y", appl [ Var "p"; Var "x" ]) ] (Var "c")
);
]
(Var "c"))
in
(* x => P(x) => exists x, P(x) *)
let exists_intro =
lam'
[
("a", Star);
("p", pi "x" (Var "a") Star);
("x", Var "a");
("y", appl [ Var "p"; Var "x" ]);
]
(lam'
[
("c", Star);
( "f",
pi' [ ("x", Var "a"); ("y", appl [ Var "p"; Var "x" ]) ] (Var "c")
);
]
(appl [ Var "f"; Var "x"; Var "y" ]))
in
check_type exists_intro
(pi'
[
("a", Star);
("p", pi "x" (Var "a") Star);
("x", Var "a");
("y", appl [ Var "p"; Var "x" ]);
]
(appl [ exists; Var "a"; Var "p" ]));
(* not (exists x, P(x)) *)
let not_exists = appl [ negate; appl [ exists; Var "a"; Var "p" ] ] in
(* forall y, not (P(y)) *)
let forall_not =
appl
[
forall;
Var "a";
lam "y" (Var "a") (appl [ negate; appl [ Var "p"; Var "y" ] ]);
]
in
(* not (exists x, P(x)) => forall y, not (P(y)) *)
check_type
(lam'
[ ("a", Star); ("p", pi "x" (Var "a") Star); ("x", not_exists) ]
(lam'
[ ("y", Var "a"); ("z", appl [ Var "p"; Var "y" ]) ]
(appl
[
Var "x";
appl [ exists_intro; Var "a"; Var "p"; Var "y"; Var "z" ];
])))
(pi'
[ ("a", Star); ("p", pi "x" (Var "a") Star); ("x", not_exists) ]
forall_not)
let classical_logic () =
(* The same as in our intuitionistic logic. *)
let absurdity = pi "a" Star (Var "a") in
let negate = lam "a" Star (pi "x" (Var "a") absurdity) in
let dn = appl [ negate; appl [ negate; Var "a" ] ] in
(* not (not A) => A; double negation law (DN) *)
let dn_law = pi' [ ("a", Star); ("y", dn) ] (Var "a") in
(* We can use CoC as a metacalculus for classical logic, by injecting either
DN or ET (excluded third) into the context as axioms. However, for the sake
of brevity, here we only deal with DN. *)
check_type
~ctx:[ ("dn", dn_law); ("a", Star); ("x", dn) ]
(appl [ Var "dn"; Var "a"; Var "x" ])
(Var "a");
let not_a = appl [ negate; Var "a" ] in
(* (not A => A) => A *)
check_type
~ctx:[ ("dn", dn_law) ]
(lam'
[ ("a", Star); ("x", pi "y" not_a (Var "a")) ]
(appl
[
Var "dn";
Var "a";
lam "z" not_a (appl [ Var "z"; appl [ Var "x"; Var "z" ] ]);
]))
(pi' [ ("a", Star); ("x", pi "y" not_a (Var "a")) ] (Var "a"));
let not_a_implies_b = appl [ negate; pi "x" (Var "a") (Var "b") ] in
(* not (A => B) => A *)
check_type
~ctx:[ ("dn", dn_law) ]
(lam'
[ ("a", Star); ("b", Star); ("x", not_a_implies_b) ]
(appl
[
Var "dn";
Var "a";
lam "z" not_a
(appl
[
Var "x";
lam "v" (Var "a") (appl [ Var "z"; Var "v"; Var "b" ]);
]);
]))
(pi' [ ("a", Star); ("b", Star); ("x", not_a_implies_b) ] (Var "a"));
let a_implies_b_implies_a = pi "x" (pi "y" (Var "a") (Var "b")) (Var "a") in
(* ((A => B) => A) => A; Peirce's law *)
check_type
~ctx:[ ("dn", dn_law) ]
(lam'
[ ("a", Star); ("b", Star); ("x", a_implies_b_implies_a) ]
(appl
[
Var "dn";
Var "a";
lam "z" not_a
(appl
[
Var "z";
appl
[
Var "x";
lam "v" (Var "a") (appl [ Var "z"; Var "v"; Var "b" ]);
];
]);
]))
(pi' [ ("a", Star); ("b", Star); ("x", a_implies_b_implies_a) ] (Var "a"))
let () =
church_booleans ();
church_numerals ();
intuitionistic_logic ();
classical_logic ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment