Formal Definition of Equality

  What follows is a recursive definition of four predicates--- T type, , T=S and ---on possibly open terms. When restricted to closed terms these are just the predicates which constitute the type system. In the clauses below,

range over possibly open terms,

range over variables;

k,j range over positive integers;

m,n range over integers;

i ranges over atom constants.

T type iff T=T

iff

  iff void or atom or int

or (a=b in A) & (= in )
* & & &

or (a<b) & (<) & int & int

or A list & list &

or A|B & | & &

or ( x:A#B or A#B )
* & ( :# or # )
* & & if

or ( x:A->B or A->B )
* & ( :-> or -> )
* & & if

or
* ( {x:A|B} or {A|B} )
* & ( {:|} or {|} )
* & & u occurs in neither B nor
* & u:A->->
* & u:A->->

or
* ( x,y:A//B or A//B )
* & ( ,:// or // )
* &
* & u,v,w are distinct and occur in neither B nor
* & u:A->v:A->->
* & u:A->v:A->->
* & u:A->
* & u:A->v:A->->
* & u:A->v:A->w:A->->->
*

or Uk

  if &

not void

atom iff

int iff

(a=b in A) iff axiom &

a<b iff axiom & & & m is less than n

A list iff A list type
* & nil or (a.b) & (.)
* & & A list

A|B iff A|B type
* & ( inl(a) & inl() & )
* or inr(b) & inr() &

x:A#B iff x:A#B type
* & <a,b> & <,>
* & &

x:A->B iff x:A->B type
* & \ u.b & \ .
* &
* if

{x:A|B} iff {x:A|B} type & &

x,y:A//B iff x,y:A//B type & &
* &

Uk iff void or atom or int

or (a=b in A) & (= in )
* & Uk & &

or (a<b) & (<)
* & int & int

or A list & list & Uk

or A|B & |
* & Uk & Uk

or ( x:A#B or A#B )
* & ( :# or # )
* & Uk
* & Uk if

or ( x:A->B or A->B )
* & ( :-> or -> )
* & Uk
* & Uk if

or
* ( {x:A|B} or {A|B} )
* & ( {:|} or {|} )
* & Uk
* & Uk if
* & Uk if
* & u occurs in neither B nor
* & u:A->->
* & u:A->->

or
* ( x,y:A//B or A//B )
* & ( ,:// or // )
* & Uk
* & Uk if &
* & Uk if &
* & u,v,w are distinct and occur in neither B nor
* & u:A->v:A->->
* & u:A->v:A->->
* & u:A->
* & u:A->v:A->->
* & u:A->v:A->w:A->->->
*

or Uj & j is less than k