# 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