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