- 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) *)