Next: Support for strongly cantorian Up: Implementing stratified abstraction in Previous: The implementation of stratification

### Examples of the implementation of stratification

```- s "?x@?x";

{?x @ ?x}
?x @ ?x

- ri "BIND@?x"; ex();

{?x @ ?x}                  (* the function [?1@?1]
?x @ ?x                    violates stratification
restrictions *)

- s "[?1@?1]";

Watson:  Term is not stratified

- s "[[?1]]";              (* this is the ``function''
which sends objects to their
constant functions
(the K combinator); it cannot
be typed in this theory *)

Watson:  Term is not stratified

- s "(?f@?x)+?g@?x";

{(?f @ ?x) + ?g @ ?x}
(?f @ ?x) + ?g @ ?x

- ri "BIND@?x"; ex();

{[(?f @ ?1) + ?g @ ?1] @ ?x}
[(?f @ ?1) + ?g @ ?1] @ ?x

- left();ri "BIND@?g";ex();

{[[(?f @ ?2) + ?1 @ ?2]] @ ?g} @ ?x
[[(?f @ ?2) + ?1 @ ?2]] @ ?g

- left(); ri "BIND@?f"; ex();

(* stratification restrictions prevent this
from working; the problem is that ?f and ?g
are at the same relative type *)

({[[(?f @ ?2) + ?1 @ ?2]]} @ ?g) @ ?x
[[(?f @ ?2) + ?1 @ ?2]]

(* we show how to achieve a function with ?f and ?g
as parameters *)

- startover();

{(?f @ ?x) + ?g @ ?x}
(?f @ ?x) + ?g @ ?x

- assign "?f,?g" "(P1@?F),P2@?F";

(* the assign command will carry out
assignments based on matches of complex terms *)

(* P1 and P2 are projection operators for the pair
represented by the comma operator; their defining
axioms are predeclared *)

{((P1 @ ?F) @ ?x) + (P2 @ ?F) @ ?x}
((P1 @ ?F) @ ?x) + (P2 @ ?F) @ ?x

- ri "BIND@?x"; ex();

{[((P1 @ ?F) @ ?1) + (P2 @ ?F) @ ?1] @ ?x}
[((P1 @ ?F) @ ?1) + (P2 @ ?F) @ ?1] @ ?x

- left(); ri "BIND@?F"; ex();

(* the abstract on the left is a pure abstract
which handles addition of functions *)

{[[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?F} @ ?x
[[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?F

(* we demonstrate application
and evaluation of this abstract *)

- assign "?F" "?f,?g";

{[[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?f , ?g}
@ ?x

[[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?f , ?g

- ri "EVAL"; ex();

{EVAL => [[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?f
, ?g} @ ?x
EVAL => [[((P1 @ ?1) @ ?2) + (P2 @ ?1) @ ?2]] @ ?f
, ?g

- left();left();left();

[({P1 @ ?f , ?g} @ ?1) + (P2 @ ?f , ?g) @ ?1] @ ?x
P1 @ ?f , ?g

- ri "P1"; ex();

[({?f} @ ?1) + (P2 @ ?f , ?g) @ ?1] @ ?x
?f

- up();up();right();left();

[(?f @ ?1) + {P2 @ ?f , ?g} @ ?1] @ ?x
P2 @ ?f , ?g

- ri "P2"; ex();

[(?f @ ?1) + {?g} @ ?1] @ ?x
?g

- top(); ri "EVAL"; ex();

{(?f @ ?x) + ?g @ ?x}
(?f @ ?x) + ?g @ ?x

(* Here's something which ought to be allowed -- we'll
show how to fix this in the next section *)

- s "forall@[forsome@[?1=?2]]";

Watson:  Term is not stratified

(* the term above represents the sentence ``for all x,
for some y, x = y'', which certainly ought to be
meaningful (and, as we will see below, Watson will
treat this as stratified, given further information) *)
```

Randall Holmes
2000-11-03