CSE 360: Lecture 2

ML types as propositional logic formulas

- val I = fn x => x
= and K = fn x => fn y => x
= and B = fn f => fn g => fn x => (g (f x))
= and C = fn f => fn x => fn y => (f y x)
= and S = fn x => fn y => fn z => ((x z) (y z));
val I = fn : 'a -> 'a
val K = fn : 'a -> 'b -> 'a
val B = fn : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
val C = fn : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val S = fn : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
-

Notice that all of these types correspond to tautologies (identify -> with implication). Use truth-tables or try forming an argument to see why they represent true formulas.

If you are allowed only application and lambda-abstraction ( fn), then how many functions are there of the following types?

'a -> 'a
'a -> 'a -> 'a
'a -> 'b -> 'a

Introducing Conjunctions into Types

- abstype ('a,'b) conj = c of 'a * 'b
=  with
=   fun pair x y = c(x,y)
=   fun left (c(x,y)) = x
=   fun right(c(x,y)) = y
=  end;
type ('a,'b) conj
val pair = fn : 'a -> 'b -> ('a,'b) conj
val left = fn : ('a,'b) conj -> 'a
val right = fn : ('a,'b) conj -> 'b

- (* Prove: (a -> b) -> (a and c) -> b  *)


- fun p1 x y = (x (left y));
val p1 = fn : ('a -> 'b) -> ('a,'c) conj -> 'b


- (* Prove: ((a -> b) and (a -> c)) -> a -> (b and c) *)


- fun p2 x y = pair ((left x) y) ((right x) y);
val p2 = fn : ('a -> 'b,'a -> 'c) conj ->
                            'a -> ('b,'c) conj


- (* Prove: (a and b) -> (b and a)  *)


- fun p3 x = pair (right x) (left x);
val p3 = fn : ('a,'b) conj -> ('b,'a) conj
-

Introducing Disjunctions into Types

- abstype ('a,'b) or = left of 'a | right of 'b
=  with fun putl x = left x
=   fun putr x = right x
=   fun cases (left x)  f g = f x
=     | cases (right x) f g = g x
= end;
type ('a,'b) or
val putl = fn : 'a -> ('a,'b) or
val putr = fn : 'a -> ('b,'a) or
val cases = fn : ('a,'b) or -> ('a -> 'c) ->
                               ('b -> 'c) -> 'c

- (* Prove:  (a or b) -> (b or a)   *)
- fun q1 x = cases x putr putl;
val q1 = fn : ('a,'b) or -> ('b,'a) or


- fun q1 x = cases x (fn y => (putr y))
                     (fn y => (putl y));
val q1 = fn : ('a,'b) or -> ('b,'a) or


- (* Prove: (a or b) -> (a -> c) ->
                        (b and d -> c) -> d -> c  *)
- fun q2 x y z w = cases x (fn n => (y n))
                           (fn m => (z (pair m w)));
val q2 = fn : ('a,'b) or -> ('a -> 'c) ->
              (('b,'d) conj -> 'c) -> 'd -> 'c

Typing Rules for ML Programs

Typing Rules for ML Programs Containing only application, abstraction, pair, left, right, putl, putr, and cases.

                                 (x : a)

t : a -> b   s : a                t : b
__________________        ____________________
    (t s) : b             (fn x => t) : a -> b


  t : a    s: b         t : (a,b) conj   t : (a,b) conj
_____________________    ____________    _____________
pair(t,s) : (a,b) conj   (left t) : a    (right t) : b


       t : a                     t : b
____________________      ____________________
(putl t) : (a, b) or      (putr t) : (a, b) or


  t : (a, b) or   f : a -> c   g : b -> c
  _______________________________________
           (cases t f g) : c

Inference Rules for Propositional Logic

Where the logic contains only implication, conjunction, and disjunction.

(a) a -> b a b __________ ________ b a -> b

a b a and b a and b __________ _______ _______ a and b a b a b ______ ______ a or b a or b

a or b a -> c b -> c ____________________________ c

These rules are examples of natural deduction inference rules, of which we shall return later.

Proofs and Programs

To find a program of the type

  ('a -> 'b,'a -> 'c) or -> 'a -> ('b,'c) or

consider how you might prove it as a formula. This leads naturally to the program

- fn x =>(fn y => cases x (fn z=> putl(z y))
                          (fn z=> putr(z y)));

Clearly, programs correspond to proofs, and types correspond to propositional logic formulas.

This correspondence is called by various names:

formulas-as-type
proofs-as-programs
the Curry-Howard Isomorphism

Here the logic for which the types correspond most closely is intuitionistic propositional logic (which we shall study in detail later).

Proofs and Programs (another example)

(a, b) or -> (a -> c) -> (b * d -> c) -> d -> c

                                    b     d
                                    _______
                       b * d -> c    b * d
                       ___________________                     
                                  c
                               _______
(a, b) or      a -> c           b -> c
______________________________________
                 c
               ______
               d -> c
       ________________________
       ((b * d) -> c) -> d -> c
   ____________________________________
   (a -> c) -> ((b * d) -> c) -> d -> c
________________________________________________
(a,b) or -> (a -> c) -> ((b * d) -> c) -> d -> c


- fn x => fn y => fn z => fn w =>
=   (cases x y (fn m => (z (m,w))));

ML typing is weaker than classical Logic

Take provability to mean (informally) that there is a ``pure'' ML program that has that type.

Take truth (informally) to mean that the formula satisfies all truth assignments (via truth tables).

We shall show later that soundness holds.

Soundness: If B is the type of a ``pure'' ML program, then M is true.

Completeness is not true. That is, there are true formulas that are not the type of any ML program. This is true of the following types.

(('a -> 'b) -> 'a) -> 'a

('a -> 'b -> 'c) -> ('a -> 'c, 'b -> 'c) or

ML typing corresponds to intuitionistic logic while truth tables correspond to classical logic. Thus, classical logic is not adequate for describing ML typing.

The order of a propositional formulas

clausal(A) = 0, provided A is atomic or T}
clausal(B1 and B2) = max(clausal(B1), clausal(B2))
clausal(B1 or B2) = max(clausal(B1), clausal(B2))
clausal(B1 => B2) = max(clausal(B1)+1, clausal(B2))

Clearly this same definition can be applied to get the order of a type.

clausal(a) = 0
clausal(a  =>  b =>  c) = 1
clausal((a  =>  b) =>  b) = 2
clausal((a or b) => (a =>  c) => (b =>  c) =>  c) = 2
clausal(((p  =>  q) =>  p) =>  p) = 3

The order of a formula (or type) is the max depth of nesting of => (or ->) to the left.

When constructors have types of order 0 and 1

- datatype a = f of b * c | g of a * b
                          | h of a * a | x | y
= and      b = u of a | v
= and      c = i of a * c | j of a | w;
datatype  a
  con f : b * c -> a
  con g : a * b -> a
  con h : a * a -> a
  con x : a
  con y : a
datatype  b
  con u : a -> b
  con v : b
datatype  c
  con i : a * c -> c
  con j : a -> c
  con w : c
- f(u(h(x,y)), j x);
val it = f (u (h (#,#)),j x) : a
- i(g(x,v),j y);
val it = i (g (x,v),j y) : c
-

When all type constructors have types of order 0 or 1, then lambda-abstractions are not needed. Such terms are often called first-order terms.

When all type constructors are of order 0 then that type is an enumerated type.

When constructors have types of order 2

- datatype d = p of d * d | q of d -> d;
datatype  d
  con p : d * d -> d
  con q : (d -> d) -> d
- q (fn z => z);
val it = q fn : d
- q (fn z => p(z,z));
val it = q fn : d
- q (fn z => q ( fn y => p(z,p(z,y))));
val it = q fn : d
- q (fn z => q (fn y => p(z,p(z, q (fn z => z)))));
val it = q fn : d
-

Here, the type of q is of second-order and ML's lambda-abstraction is needed to build terms of type d.

Notice that ML will not print the structure of lambda-terms. lambda Prolog allows for the structure of lambda-terms to be analyzed.

Lecture Directory / Module Directory / CSE360 Syllabus