Caml types and intuitionistic logic

A project by Dale Miller

Dale.Miller @ inria.fr

1  Goal

The goal of this project is to use a theorem prover for propositional intuitionistic logic in order to answer questions about a collection of Caml types. In particular, if one is given a list of Caml types (none of which are polymorphic) and a particular ``target'' type, one would like to know if it is possible to build a ``simple'' Caml program of that target type from that list of types.

2  Background

By simple Caml program over Δ, we shall mean an Caml program built from constants in Δ using just application, abstraction, and the constructors for conjunction and disjunction. Here, conjunction is specified using the conj type and disjunction is specified using the disj type.
# type ('a,'b) conj = Pair of 'a * 'b;;
type ('a, 'b) conj = Pair of 'a * 'b
# let left  = function (Pair(x,y)) -> x;;
val left : ('a, 'b) conj -> 'a = <fun>
# let right = function (Pair(x,y)) -> y;;
val right : ('a, 'b) conj -> 'b = <fun>
# type ('a,'b) disj = Putl of 'a | Putr of 'b;;
type ('a, 'b) disj = Putl of 'a | Putr of 'b
# let cases = function (Putl x,f,g) -> f x | (Putr x,f,g) -> g x;;
val cases : ('a, 'b) disj * ('a -> 'c) * ('b -> 'c) -> 'c = <fun>
# 
Notice that it is possible to use simple Caml programs as proofs of propositional formulas. Consider, for example, the following Caml programs.
     (*  Prove: ((a or b) -> c) -> a -> c  *)
# let p1 x y = (x (Putl y));;
val p1 : (('a, 'b) disj -> 'c) -> 'a -> 'c = <fun>
     (* Prove: ((a -> b) and (a -> c)) -> a -> (b and c) *)
# let p2 x y = Pair ((left x) y,(right x) y);;
val p2 : ('a -> 'b, 'a -> 'c) conj -> 'a -> ('b, 'c) conj = <fun>
     (* Prove: (a and b) -> (b and a)  *)
# let p3 x = Pair(right x, left x);;
val p3 : ('a, 'b) conj -> ('b, 'a) conj = <fun>
     (* Prove:  (a or b) -> (b or a)   *)   
# let q1 x = cases(x, (fun y -> (Putr y)),(fun y -> (Putl y)));;
val q1 : ('a, 'b) disj -> ('b, 'a) disj = <fun>
     (* Prove: (a or b) -> (a -> c) -> (b and d -> c) -> d -> c  *)
# let q2 x y z w = cases(x, (fun n -> (y n)), 
                            (fun m -> (z (Pair(m,w)))));;
val q2 : ('a, 'b) disj -> ('a -> 'c) -> 
         (('b, 'd) conj -> 'c) -> 'd -> 'c = <fun>
# 
Thus, for example, the Caml code q2 can be seen as a proof of the formula propositional formula
(ab)⊃ (ac)⊃ ((bd)⊃ c)⊃ dc,
where ⊃ denotes implication (replaces the function space arrow -> and where ∨ and ∧ denote disjunction and conjunction (respectively). (Notice that ⊃ and -> both associate to the right.) The proof described by q2 might be read as follows: Assume that we are given the four formulas
ab,     ac,     (bd)⊃ c,     d
and try to prove c. We need to do a case analysis: if a is true, then, using the second displayed formula, we conclude c immediately. In the other case where b is true, we first must conclude bd (since d is given as the fourth formula above) and then, using the third formula, we can conclude c also. Thus, in either case, we have established c. Notice that the structure of q2 is rather similar to the structure of this informal proof.

This connection between types and formulas is often called the Curry-Howard Isomorphism.

3  Allowing other typed constants

Now consider the problem of having a library of Caml programs for which you have easy access to their types. (We shall assume that this library does not contain constants of polymorphic type.) For example, assume you have the following typed symbols:
type f : int -> list bool
type g : list int -> int -> int
type h : (bool -> int) -> list bool -> list int
type u : bool -> int
type v : (int, real) or -> complex
type m : string -> int
type n : string -> real
One might try to use your solution to this project to answer the following questions: Is there a term of type int -> list int? Of type list int -> int? Of type string -> complex? Of type complex -> string? Etc.



Given the discussion before, all of these questions have a parallel in logic. For example, given the propositional formulas
int ⊃ listbool     listint ⊃ int ⊃ int     (bool ⊃ int) ⊃ listbool ⊃ listint
bool ⊃ int     (int ∨ real) ⊃ complex     string ⊃ int     string ⊃ real
is it possible to prove the formula string⊃ complex? (Notice also that (list bool) is treated as a propositional symbol listbool.) If there is a proof, the proof should describe a simple Caml program. If there is no such proof, then there is no such program. This formal connection is part of the theory of the Curry-Howard Isomorphism.



Figure 1 : Inference rules in sequent style for propositional logic [Dyc92]. The rule ⊃L1 has the additional requirement that the formula B is a propositional symbol.



4  A proof system for propositional intuitionistic logic

Thus, to answer the questions about whether or not a simple Caml program of a given type can exist given a collection of (non-polymorphic) Caml constants, we can instead try to answer the questions whether or not a given propositional formula follows from a set of other propositional formulas using the rules for intuitionistic logic. Provability of propositional intuitionistic logic has been well studied. Provability is known to be decidable.

A common way to present a proof system for a logic is to use sequent calculus. For this project, we assume that a sequent is a pair, written as Δ —→ G where G is a propositional formula and Δ is a multiset of propositional formulas. [Recall that a multiset is a set in where objects have a multiplicity: equivalently, they are list structures in which order does not matter.] A sequent Δ —→ G denotes, in a sense, the attempt to proved the formula G from the formulas in Δ: if you will, consider doing a mathematical proof where at the top of your paper you write the assumptions (here, Δ) and at the bottom, the statement you would like to proved from these assumption (here, G).

A sequent calculus proof system for this logic is given Figure 1 and is due to R. Dyckhoff [Dyc92]. Consider using these rules to search for a proof in intuitionistic logic. That is, think of starting with a given sequent, consider what inference rule could give rise to that sequent. Generally, such an inference rule will give rise to one or two additional sequents that need to be proved as well. The entire proof search process terminates when all remaining sequents are justified by the initial rule.

In Figure 1, a few inference rules are marked with a dag . This means that the conclusion of this inference rule is provable if and only if the premises are provable. Thus, for the purpose of searching for a proof, one does not need to backtrack on the selection of these rules: if they can apply, then apply them and consider no other choice of inference rule. All other rules may require backtracking.

5  The actual project

Please implement in a high-level language (preferably Caml, OCaml, or Java) the following steps.
  1. Build a lexical analyzer and parser that will read a collection of typed Caml constants (a signature) denoting Γ and another Caml type denoting A.

  2. Implement the proof search mechanism described by the sequent system in Figure 1 for the sequent Γ —→ A.

  3. Report your answer to the user: that is, tell the user whether or not a simple Caml program of type A exists using constants in the list Γ.

  4. If an such an Caml program exists, print out one.

  5. Develop a good example illustrating the usefulness of your system.

Références

[Dyc92]
Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795--807, September 1992.

Ce document a été traduit de LATEX par HEVEA.