.ds G1 Unclassified \" classification
.ds G2 DBC/RBJ/076 \" reference
.ds G3 0.1 \" Issue Number
.ds G4 ? \" Pages
.ds G5 Draft \" status
.ds G6 Combinatory Type Theory in HOL \" title
.ds G7 Formal Theory\" document type
.ds G8 COMBINATORY-LOGIC TYPE-THEORY HOL \" keywords
.ds G9 R.B.Jones
.\" used p1 - p0 - u4 as string registers for proof step labels
.nr HM 0i
.nr HM 0i
.ds CH
.ds CF
.de F2 \" line across page
.sp
\l'6i'
.sp
..
.de F1
.F2
.LP
\fBDistribution: \fR* = top sheet only
.LP
.br
.ce
\s+3\*(G1\s-3
..
.TS \" Header
expand tab(%);
cp14 s s s
cp14 s s s
lp36 l l l
^ l l l
cp14 l l l
cp14 ^ ^ ^.
\*(G1

I C L %Defence%Technology%Formal
\^%Business%Development%Methods
Defence%Centre%Department%
Systems%%%
.TE
.F2
.TS \" Document information
tab(%) center;
lfB l lfB l lfB l
lfB l lfB l lfB l
lfB l lfB l lfB l
lfB l lfB l lfB l
lfB l s s s s
lfB l s s s s
lfB l s s s s
lfB l s s s s
lfB l s s s s
lfB l s s s s
lfB l s s s s
lfB l s s s s.
Ref:%\*(G2%Issue:%\*(G3%Pages:%\*(G4

Date:%1988-02-04%Status:%\*(G5

Title:%T{
.UL "\*(G6"
T}

Prepared by:%\*(G9

Document Type:%\*(G7

Keywords:%\*(G8
.TE
.F2
.TS \" Sign-off box, one line per signer, at end
tab(%) center box;
cBp12 s s
lp12w(1.3i) | lp12w(1.3i) | lp12w(2i)
lp12 | lp12 | lp12.
Sign-off Authority
_
Name%Location%    Signature
_

.TE
.F2
.LP
.B
Summary:
.R
.LP \" Document Summary
This document contains a formal development of a combinatory type theory
in Higher Order Logic (HOL).
.LP
.wh -15 F1 \" distance from bottom of page for distribution list
.bp 3
.ch F1
.nr HM 1i
.nr FM 1i
.TL
\*(G6
.AU
\*(G9
.AI
Formal Methods Group,
ICL Defence Systems.
.LP
.so roff.defs
.ds OH
.ds EH
.ds EF
.ds OF
.ds CH 
.ds LH \*(G6
.ds RH 1988-02-04
.ds CF
.ds LF \*(G2 Issue \*(G3
.ds RF Page %
.nr PS 11
.nr VS 14
.LP
.NH
INTRODUCTION
.LP
The combinatory terms are the free algebra generated by the 2-ary
operator Ap from the 0-ary constants K,S,\(*C and a countable set
of 0-ary variables (Va n), for n\(monum.
.LP
Pure combinators are combinatory terms in which there occurs no 0-ary
consitituents except K and S.
.LP
The combinators are our primitive language in which we assert propositions.
The subject matter of these propositions is the pure combinators, and
ranges, pacs, types, and type_assignments which may be represented, or
approximated by pure combinators.
.LP
.hd
new_theory(`076`);;
.he
.NH
REPRESENTING COMBINATORS BY NUMBERS
.LP
In order to use HOL as a metalanguage we must determine some way to represent
the objects in the language as objects in HOL.
.LP
This is done using the type "num" consisting of the natural numbers 0,1,2...
0,2 and 4 represent respectively K, S, \(*C, and the remaining even numbers
are used to represent variables.
Odd numbers are used to represent applications, using the bijection:
(n,m)->(n+m)(n+m)+(2nm)+n+3m+1.
Projections are defined, pro-tem, using the choice function \(*m.
.hd
new_definition(`K_DEF`,
	"K = 0"											);;
new_definition(`S_DEF`,
	"S = 2"											);;
new_definition(`\(*C_DEF`,	
	"\(*C = 4"											);;
.he
.hd
new_definition(`Va_DEF`,
	"(Va:num\(->num) n = 6+(2*n)"							);;
new_infix_definition(`Ap_DEF`,
	"(Ap:num\(->num\(->num) n m = (n*n)+(m*m)+(2*n*m)+n+(3*m)+1"	);;
.he
.hd
new_definition(`is_atom_DEF`,
	"(is_atom:num\(->bool) n = \*kx.n=2*x"						);;
new_definition(`is_Ap_DEF`,
	"(is_Ap:num\(->bool) n = \(no is_atom n"						);;
.he
.hd
new_definition(`fun_DEF`,
	"(fun:num\(->num) n = \(*mx.\*ky.n=x Ap y"						);;
new_definition(`arg_DEF`,
	"(arg:num\(->num) n = \(*my.\*kx.n=x Ap y"						);;
.he
.NH
CONVERSION
.LP
The combinators are to be used to represent functions over combinators.
The first step in showing how this is done consists in defining an equivalence
relation over the combinatory terms.
Operationally the semantics of combinators as representing functions is
determined by a graph reduction process.
If this graph reduction process is regarded as preserving equality in some
way, then the strongest equality compatible with the normal reduction rule
for K and S is the equivalence relation which we define below as 'conv'.
.LP
'conv' is defined as the smallest applicative equivalence relation containing
the basic reduction rules for K and S.
We therefore first define an equivalence relation, then an applicative
relation, the relation of immediate reducibility, and finally 'conv'.
.NH 2
Equivalence Relations
.hd m
let relation = ":*num\(->*num\(->bool";;
let numeric_relation = ":num\(->num\(->bool";;
.he
.hd
new_definition(`reflexive_DEF`,"(reflexive:^relation\(->bool) r =
	\*jx:*num.r x x");;
new_definition(`symmetric_DEF`,"(symmetric:^relation\(->bool) r =
	\*jx y.r x y \(rh r y x");;
new_definition(`transitive_DEF`,"(transitive:^relation\(->bool) r =
	\*j(x:*num)(y:*num)(z:*num).(r x y) \*e (r y z) \(rh (r x z)");;
new_definition(`equivalence_DEF`,"(equivalence:^relation\(->bool) r =
	reflexive r \*e symmetric r \*e transitive r");;
new_infix_definition(`contains_DEF`,"($contains:^relation\(->^relation\(->bool) r1 r2 =
	\*jx y. r2 x y \(rh r1 x y");;
new_definition(`equivalence_closure_DEF`,
	"(equivalence_closure:^relation\(->^relation) r =
	\(*ms. equivalence s \*e s contains r \*e
	\*jt:^relation. equivalence t \*e t contains r \(rh t contains s");;
.he
.NH 2
Applicative Relations
.hd
new_definition(`applicative_DEF`,"(applicative:^numeric_relation\(->bool) r =
	\*jx x' y y'. (r x x' \*e (r y y' \*d (y=y'))) \*d ((x=x') \*e (r y y'))
	\(rh r (x Ap y) (x' Ap y')");;

new_definition(`applicative_closure_DEF`,
	"(applicative_closure:^numeric_relation\(->^numeric_relation) r =
	\(*ms. applicative s \*e s contains r \*e
	\*jt:^numeric_relation. applicative t \*e t contains r \(rh t contains s");;
.he
.NH 2
Immediate Reducibility and Conversion
.LP
.hd
new_definition(`prim_red_DEF`,"(prim_red:num\(->num\(->bool) x y =
	(\*ku. x = (K Ap y) Ap u) \*d
	\*ku v w. x = ((S Ap u) Ap v) Ap w");;
new_infix_definition(`im_red_DEF`,"($im_red:num\(->num\(->bool)
	= (applicative_closure prim_red)");;
.he
.hd
new_infix_definition(`conv_DEF`,"($conv:num\(->num\(->bool)
	= (equivalence_closure $im_red)");;
.he
.NH
SUBSTITUTION
.LP
.hd
new_definition(`subst_DEF`,"(subst:num\(->num\(->num\(->num) =
	\(*mf. \*jx y z.
		((z = y) \(rh (f x y z = x)) \*e
		(\(no(z = y) \(rh 
			((is_atom z) \(rh (f x y z = z)) \*e
			((is_Ap z) \(rh (f x y z = ((f x y (fun z)) Ap (f x y (arg z))))))");;
new_definition(`value_DEF`,"(value:num\(->num\(->num\(->bool) x y z =
	(subst y \(*C x) conv z");;
.he
.NH
ENCODINGS
.LP
.hd
new_definition(`I_DEF`,"I = (S Ap K) Ap K");;
new_definition(`cabs_DEF`,"(cabs:num\(->num\(->num) =
	\(*mf.\*jvar body.
	((Va var = body) \(rh (f var body = I)) \*e
	(\(no(Va var = body) \(rh
		((is_atom body \(rh (f var body = body)) \*e
		(is_Ap body \(rh
			(f var body = (f var (fun body)) Ap (f var (arg body))))))");;
new_prim_rec_definition(`cabsn_DEF`,"
	(cabsn 0 n = n)	\*e
	(cabsn (SUC m) n = cabs m (cabsn m n))");;
.he
.hd
new_definition(`ctrue_DEF`,
			"ctrue = K");;
new_definition(`cfalse_DEF`,
			"cfalse = cabsn 1 (Va 0)");;
new_definition(`cif_DEF`,
			"cif x y z = ((x Ap y) Ap z)");;
new_definition(`cpair_DEF`,
			"cpair x y = cabs 0 (cif (Va 0) x y)");;
new_definition(`cfst_DEF`,
			"cfst x = x Ap ctrue");;
new_definition(`csnd_DEF`,
			"csnd x = x Ap cfalse");;
.he
.hd
new_definition(`encode_DEF`,"encode:num\(->num =
	\(*m f.\*jx.
		((x=K)\(rh (f x = cpair ctrue ctrue)) \*e
		((x=S)\(rh (f x = cpair ctrue cfalse)) \*e
		(is_Ap x \(rh (f x = cpair cfalse (cpair (f (cfst x))(f (csnd x)))))");;
.he
.NH
INTERPRETATIONS
.LP
I now want to define the acceptable interpretations of \(*C.
Informally \(*C should be understood as a function which takes two encodings
of combinators and returns true if the range represented by the first is
contained in the range represented by the second, otherwise it returns false.
This function is not recursive, so we have to accept an approximation.
An approximation is a function which never yields an incorrect truth value,
but may sometimes yield no truth value.
.LP
We may use combinators to represent and number of different things.
.NH 2
Ranges
.LP
First a combinator may represent a range, by which should be understood
a range of quantification.
.hd m
let range = ":num\(->bool";;
.he
.hd
new_definition(`comb_to_range`,"(comb_to_range:num\(->^range) x y =
	(x Ap (encode y)) conv ctrue");;
.he
.LP
A fundamental relation over ranges is inclusion:
.hd
new_definition(`rnge_incl`,"(rnge_incl:^range\(->^range\(->bool) r s =
	(\*jx. r x \(rh s x)");;
.he
.LP
\(*C is intended to approximate `rnge_incl` in the object language.
Since `rng_incl` is not recursive (or recursively enumerable), we
have to accept computable approximations.
.LP
Second a combinator may represent a partial characteristic function,
which we abbreviate, pac.
.hd m
let pac = ":num\(->(bool#bool)";;
.he
.LP
The type of an approximation is a partial relation over ranges:
.hd m
let approxim = ":^range\(->^range\(->(bool#bool)";;
.he
.LP
And the perfect 'approximation' to \(*C is:
.hd
new_definition(`pox\(*C`,"(pox\(*C:^approxim) r s =
	let b = rnge_incl r s in (b,\(nob)");;
.he
.LP
Since every combinator represents a range this induces a partial
relation over combinators as follows:
.hd m
let approximc = ":num\(->num\(->(bool#bool)";;
.he
.hd
new_definition(`pox\(*Cc`,"(pox\(*Cc:^approximc) x y =
	pox\(*C (comb_to_range x) (comb_to_range y)");;
.he
.LP
We now define a partial ordering over these approximations:
.hd
new_infix_definition(`better_than`,"($better_than:^approximc\(->^approximc\(->bool) a b =
	\*j(x:num) (y:num).	let a_yes = FST (a x y) in
			let a_no = SND (a x y) in
			let b_yes = FST (b x y) in
			let b_no = SND (b x y) in
			((b_yes \(rh a_yes) \*e (b_no \(rh a_no)) ");;
.he
.LP
A combinator when regarded as a partial characteristic function over
encoded terms determines a 'partial relation' over combinators as follows: 
.hd
new_definition(`comb_to_prel`,"(comb_to_prel:num\(->^approximc) n x y =
	((n Ap (encode x) Ap (encode y)) conv ctrue,
	 (n Ap (encode x) Ap (encode y)) conv cfalse)");;
.he
.LP
We can now define the notion of approximation to \(*C as any combinator which
pox\(*Cc is 'better_than':
.hd
new_definition(`approx\(*C`,"(approx\(*C:num\(->bool) x =
	pox\(*Cc better_than (comb_to_prel x)");;
.he
.LP
.hd
new_infix_definition(`$better_\(*C_than`,"($better_\(*C_than:num\(->num\(->bool) x y =
	approx\(*C x
	\*e (comb_to_prel x) better_than (comb_to_prel y)");;
new_infix_definition(`true_for`,"($true_for:num\(->num\(->bool) x y =
	(subst y \(*C x) conv ctrue");;
new_definition(`valid`,"(valid:num\(->bool) x =
	\*ky. approx\(*C y \*e
	(\*jz. z better_\(*C_than y \(rh x true_for z)");;
.he
.NH
PACS
.LP
A pac is a partial characteristic function, or a pair of disjoint
recursively enumerable sets.
.LP
.NH
TYPES
.LP
The next objective is to define what a type is in this system,
and then to define a useful set of type constructors.
Informally a type is an ordered pair.
The first element is a PAC, the second an equivalence relationship
defined over the RANGE of the PAC.
.NH
LISTING OF THEORY
.DS L
The Theory 076
Parents --  HOL     
Constants --
  K ":num"     S ":num"     \(*C ":num"     Va ":num \(-> num"
  is_atom ":num \(-> bool"     is_Ap ":num \(-> bool"
  fun ":num \(-> num"     arg ":num \(-> num"
  reflexive ":(*num \(-> (*num \(-> bool)) \(-> bool"
  symmetric ":(*num \(-> (*num \(-> bool)) \(-> bool"
  transitive ":(*num \(-> (*num \(-> bool)) \(-> bool"
  equivalence ":(*num \(-> (*num \(-> bool)) \(-> bool"
  equivalence_closure
    ":(*num \(-> (*num \(-> bool)) \(-> (*num \(-> (*num \(-> bool))"
  applicative ":(num \(-> (num \(-> bool)) \(-> bool"
  applicative_closure
    ":(num \(-> (num \(-> bool)) \(-> (num \(-> (num \(-> bool))"
  prim_red ":num \(-> (num \(-> bool)"
  subst ":num \(-> (num \(-> (num \(-> num))"
  value ":num \(-> (num \(-> (num \(-> bool))"     I ":num"
  cabs ":num \(-> (num \(-> num)"     cabsn ":num \(-> (num \(-> num)"
  ctrue ":num"     cfalse ":num"
  cif ":num \(-> (num \(-> (num \(-> num))"
  cpair ":num \(-> (num \(-> num)"     cfst ":num \(-> num"
  csnd ":num \(-> num"     encode ":num \(-> num"
  comb_to_range ":num \(-> (num \(-> bool)"
  rnge_incl ":(num \(-> bool) \(-> ((num \(-> bool) \(-> bool)"
  pox\(*C ":(num \(-> bool) \(-> ((num \(-> bool) \(-> bool # bool)"
  pox\(*Cc ":num \(-> (num \(-> bool # bool)"
  comb_to_prel ":num \(-> (num \(-> (num \(-> bool # bool))"
  approx\(*C ":num \(-> bool"     valid ":num \(-> bool"     
Curried Infixes --
  Ap ":num \(-> (num \(-> num)"
  contains
    ":(*num \(-> (*num \(-> bool)) \(-> ((*num \(-> (*num \(-> bool)) \(-> bool)"
  im_red ":num \(-> (num \(-> bool)"     conv ":num \(-> (num \(-> bool)"
  better_than
    ":(num \(-> (num \(-> bool # bool)) \(->
      ((num \(-> (num \(-> bool # bool)) \(-> bool)"
  better_\(*C_than ":num \(-> (num \(-> bool)"
  true_for ":num \(-> (num \(-> bool)"     
Definitions --
  K_DEF  \*o K = 0
  S_DEF  \*o S = 2
  \(*C_DEF  \*o \(*C = 4
  Va_DEF  \*o Va n = 6 + (2 * n)
  Ap_DEF
    \*o n Ap m =
       (n * n) + ((m * m) + ((2 * (n * m)) + (n + ((3 * m) + 1))))
  is_atom_DEF  \*o is_atom n = (\*kx. n = 2 * x)
  is_Ap_DEF  \*o is_Ap n = \(nois_atom n
  fun_DEF  \*o fun n = (\(*mx. \*ky. n = x Ap y)
  arg_DEF  \*o arg n = (\(*my. \*kx. n = x Ap y)
  reflexive_DEF  \*o reflexive r = (\*jx. r x x)
  symmetric_DEF  \*o symmetric r = (\*jx y. r x y \(rh r y x)
  transitive_DEF  \*o transitive r = (\*jx y z. r x y \*e r y z \(rh r x z)
  equivalence_DEF
    \*o equivalence r = reflexive r \*e symmetric r \*e transitive r
  contains_DEF  \*o r1 contains r2 = (\*jx y. r2 x y \(rh r1 x y)
  equivalence_closure_DEF
    \*o equivalence_closure r =
       (\(*ms.
         equivalence s \*e
         s contains r \*e
         (\*jt. equivalence t \*e t contains r \(rh t contains s))
  applicative_DEF
    \*o applicative r =
       equivalence r \*e
       (\*jx x' y y'. r x x' \*e r y y' \(rh r(x Ap y)(x' Ap y'))
  applicative_closure_DEF
    \*o applicative_closure r =
       (\(*ms.
         applicative s \*e
         s contains r \*e
         (\*jt. applicative t \*e t contains r \(rh t contains s))
  prim_red_DEF
    \*o prim_red x y =
       (\*ku. x = (K Ap y) Ap u) \*d (\*ku v w. x = ((S Ap u) Ap v) Ap w)
  im_red_DEF  \*o $im_red = applicative_closure prim_red
  conv_DEF  \*o $conv = equivalence_closure $im_red
  subst_DEF
    \*o subst =
       (\(*mf.
         \*jx y z.
          ((z = y) \(rh (f x y z = x)) \*e
          (\(no(z = y) \(rh
           (is_atom z \(rh (f x y z = z)) \*e
           (is_Ap z \(rh (f x y z = (f x y(fun z)) Ap (f x y(arg z))))))
  value_DEF  \*o value x y z = (subst y \(*C x) conv z
  I_DEF  \*o I = (S Ap K) Ap K
  cabs_DEF
    \*o cabs =
       (\(*mf.
         \*jvar body.
          ((Va var = body) \(rh (f var body = I)) \*e
          (\(no(Va var = body) \(rh
           (is_atom body \(rh (f var body = body)) \*e
           (is_Ap body \(rh
            (f var body = (f var(fun body)) Ap (f var(arg body))))))
  cabsn_DEF_DEF
    \*o cabsn = PRIM_REC(\(*ln. n)(\(*lg00012 m n. cabs m(g00012 n))
  ctrue_DEF  \*o ctrue = K
  cfalse_DEF  \*o cfalse = cabsn 1(Va 0)
  cif_DEF  \*o cif x y z = (x Ap y) Ap z
  cpair_DEF  \*o cpair x y = cabs 0(cif(Va 0)x y)
  cfst_DEF  \*o cfst x = x Ap ctrue
  csnd_DEF  \*o csnd x = x Ap cfalse
  encode_DEF
    \*o encode =
       (\(*mf.
         \*jx.
          ((x = K) \(rh (f x = cpair ctrue ctrue)) \*e
          ((x = S) \(rh (f x = cpair ctrue cfalse)) \*e
          (is_Ap x \(rh (f x = cpair cfalse(cpair(f(cfst x))(f(csnd x))))))
  comb_to_range  \*o comb_to_range x y = (x Ap (encode y)) conv ctrue
  rnge_incl  \*o rnge_incl r s = (\*jx. r x \(rh s x)
  pox\(*C  \*o pox\(*C r s = (let b = rnge_incl r s in b,\(nob)
  pox\(*Cc  \*o pox\(*Cc x y = pox\(*C(comb_to_range x)(comb_to_range y)
  better_than
    \*o a better_than b =
       (\*jx y.
         let a_yes = FST(a x y)
         in
         let a_no = SND(a x y)
         in
         let b_yes = FST(b x y)
         in
         let b_no = SND(b x y) in (b_yes \(rh a_yes) \*e (b_no \(rh a_no))
  comb_to_prel
    \*o comb_to_prel n x y =
       (n Ap ((encode x) Ap (encode y))) conv ctrue,
       (n Ap ((encode x) Ap (encode y))) conv cfalse
  approx\(*C  \*o approx\(*C x = pox\(*Cc better_than (comb_to_prel x)
  $better_\(*C_than
    \*o x better_\(*C_than y =
       approx\(*C x \*e (comb_to_prel x) better_than (comb_to_prel y)
  true_for  \*o x true_for y = (subst y \(*C x) conv ctrue
  valid
    \*o valid x =
       (\*ky. approx\(*C y \*e (\*jz. z better_\(*C_than y \(rh x true_for z))
  
Theorems --
  cabsn_DEF  \*o (cabsn 0 n = n) \*e (cabsn(SUC m)n = cabs m(cabsn m n))
.DE
.KE