Combinators in OBJ

Combinators in OBJ

The following specifies a number of combinators in OBJ, with some test cases, which include proofs. obj COMBL is sort T . op __ : T T -> T [gather (E e)]. ops S K I : -> T . vars L M N : T . eq K M N = M . eq I M = M . eq S M N L = (M L)(N L). endo open . ops m n p : -> T . red S K K m == I m . red S K S m == I m . red S I I I m == I m . red K m n == S(S(K S)(S(K K)K))(K(S K K)) m n . red S m n p == S(S(K S)(S(K(S(K S)))(S(K(S(K K)))S)))(K(K(S K K))) m n p . red S(K K) m n p == S(S(K S)(S(K K)(S(K S)K)))(K K) m n p . let X = S I . red X X X X m == X(X(X X)) m . close open COMBL . ops x y z : -> T . let B = S(K S)K . red B x y z == x(y z). let w = S I I . red w x == x x . op F : -> T . let P = w(B F w). ***> red P == F P . *** fails to terminate! close

Here is the OBJ3 output from the above: awk% obj \|||||||||||||||||/ --- Welcome to OBJ3 --- /|||||||||||||||||\ OBJ3 version 2.04oxford built: 1994 Feb 28 Mon 15:07:40 Copyright 1988,1989,1991 SRI International 2002 Mar 12 Tue 5:14:11 OBJ> in comb ========================================== obj COMBL ========================================== open ========================================== ops m n p : -> T . ========================================== reduce in COMBL : ((S K) K) m == I m rewrites: 4 result Bool: true ========================================== reduce in COMBL : ((S K) S) m == I m rewrites: 4 result Bool: true ========================================== reduce in COMBL : (((S I) I) I) m == I m rewrites: 7 result Bool: true ========================================== reduce in COMBL : (K m) n == (((S ((S (K S)) ((S (K K)) K))) (K ((S K) K))) m) n rewrites: 13 result Bool: true ========================================== reduce in COMBL : ((S m) n) p == ((((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K K)))) S)))) (K (K ((S K) K)))) m) n) p rewrites: 21 result Bool: true ========================================== reduce in COMBL : (((S (K K)) m) n) p == ((((S ((S (K S)) ((S (K K)) ((S (K S)) K)))) (K K)) m) n) p rewrites: 17 result Bool: true ========================================== let X = S I . ========================================== reduce in COMBL : (((X X) X) X) m == (X (X (X X))) m rewrites: 27 result Bool: true ========================================== close ========================================== open COMBL ========================================== ops x y z : -> T . ========================================== let B = S ( K S ) K . ========================================== reduce in COMBL : ((B x) y) z == x (y z) rewrites: 6 result Bool: true ========================================== let w = S I I . ========================================== reduce in COMBL : w x == x x rewrites: 5 result Bool: true ========================================== op F : -> T . ========================================== let P = w ( B F w ) . ========================================== ***> red P == F P . *** fails to terminate! ========================================== close OBJ> q Bye. awk%

Back to CSE 230 homepage