CSE 230: Principles of Programming Languages
Solutions to Problem 2 on Midterm of 7 February

There are two basic approaches to this problem. The first is to write idiomatic OBJ code for accomplishing the same thing, but in a different way; this is not very difficult. The second approach is to model the Post system rather exactly, with strings as the basic data type, and with each rule as an operation on strings; this is the most faithful to the question (but it runs incredably slowly if id: nil is used instead of idr: nil). Here computations are sequences of deductions, i.e. proofs in the Post system. There is also a hybrid approach, which combines aspects other two, modeling rules as operations, but taking advantage of OBJ's power for defining data types; it runs quickly, and again, its computations are Post system proofs. Here is a link to the midterm (in postscript).

1. Code for the first approach

obj RAT is sorts Nat Rat . op N : -> Nat . op _| : Nat -> Nat . op _+_ : Nat Nat -> Nat . op _*_ : Nat Nat -> Nat . op _Q_ : Nat Nat -> Rat . op _=*=_ : Rat Rat -> Bool . vars x y z w : Nat . eq N + x = x . eq x | + y = (x + y)| . eq N * x = N . eq x | * y = (x * y) + y . eq x Q y =*= z Q w = x * w == y * z . endo red (N |) Q (N | |) =*= (N | |) Q (N | | | |).

2. Code for the second approach

obj RatPost is sort St . vars u v w x y z : St . ops nil N | * e Q : -> St . op __ : St St -> St [assoc id: nil]. op [1] : -> St . eq [1] = N . op [2]_ : St -> St . eq [2](N x) = N x | . op [4]_ : St -> St . eq [4](N x) = * x e . op [5]_ : St -> St . eq [5](x * y e z) = (x | * y e z y). op [6]__ : St St -> St . eq [6](N x) (N y) = (x Q y). op [7]___ : St St St -> St . eq [7](w Q x) (y Q z) (w * z e x * y) = (w Q x e y Q z) . op [8]__ : St St -> St . eq [8](x * y e z) (u * v e z) = (x * y e u * v). endo open . let n0 = [1] . let n1 = [2] n0 . let n2 = [2] n1 . let n3 = [2] n2 . let n4 = [2] n3 . let q1 = [6] n1 n2 . let q2 = [6] n2 n4 . let e1 = [5][5][4] n2 . let e2 = [5][4] n4 . let e3 = [8] e2 e1 . let e4 = [7] q1 q2 e3 . red n4 . red q2 . red e1 . red e2 . red e3 . red e4 . close

3. Code for the third approach

obj RatPost is sorts Nat NatN Term Eq Rat . subsort Nat < Term . vars u v w x y z : Nat . ops nil | : -> Nat . op __ : Nat Nat -> Nat [assoc id: nil]. op N_ : Nat -> NatN . op _*_ : Term Term -> Term . op _e_ : Term Term -> Eq [comm]. op _e_ : Rat Rat -> Eq . op _Q_ : Nat Nat -> Rat . op [1] : -> NatN . eq [1] = N nil . op [2]_ : NatN -> NatN . eq [2](N x) = N (x |). op [4]_ : NatN -> Eq . eq [4](N x) = (nil * x) e nil . op [5]_ : Eq -> Eq . eq [5]((x * y) e z) = (x | * y) e (z y). op [6]__ : NatN NatN -> Rat . eq [6](N x) (N y) = (x Q y). op [7]___ : Rat Rat Eq -> Eq . eq [7](w Q x) (y Q z) ((w * z) e (x * y)) = (w Q x) e (y Q z) . op [8]__ : Eq Eq -> Eq . eq [8]((x * y) e z) ((u * v) e z) = (x * y) e (u * v). endo open . let n0 = [1] . let n1 = [2] n0 . let n2 = [2] n1 . let n3 = [2] n2 . let n4 = [2] n3 . let q1 = [6] n1 n2 . let q2 = [6] n2 n4 . let e1 = [5][5][4] n2 . let e2 = [5][4] n4 . let e3 = [8] e2 e1 . let e4 = [7] q1 q2 e3 . red n4 . red q2 . red e1 . red e2 . red e3 . red e4 . close

4. Output for the first approach

awk% obj \|||||||||||||||||/ --- Welcome to OBJ3 --- /|||||||||||||||||\ OBJ3 version 2.04oxford built: 1994 Feb 28 Mon 15:07:40 Copyright 1988,1989,1991 SRI International 2002 Feb 25 Mon 3:29:10 OBJ> in rat ========================================== obj RAT ========================================== reduce in rat : ((N |) Q ((N |) |)) =*= (((N |) |) Q ((((N |) |) |) |)) rewrites: 12 result Bool: true OBJ> q Bye. awk%

5. Output for the second approach

awk% obj \|||||||||||||||||/ --- Welcome to OBJ3 --- /|||||||||||||||||\ OBJ3 version 2.04oxford built: 1994 Feb 28 Mon 15:07:40 Copyright 1988,1989,1991 SRI International 2002 Feb 25 Mon 7:27:31 OBJ> in ratpost1 ========================================== obj RatPost ========================================== open ========================================== let n0 = [ 1 ] . ========================================== let n1 = [ 2 ] n0 . ========================================== let n2 = [ 2 ] n1 . ========================================== let n3 = [ 2 ] n2 . ========================================== let n4 = [ 2 ] n3 . ========================================== let q1 = [ 6 ] n1 n2 . ========================================== let q2 = [ 6 ] n2 n4 . ========================================== let e1 = [ 5 ] [ 5 ] [ 4 ] n2 . ========================================== let e2 = [ 5 ] [ 4 ] n4 . ========================================== let e3 = [ 8 ] e2 e1 . ========================================== let e4 = [ 7 ] q1 q2 e3 . ========================================== reduce in RatPost : n4 rewrites: 10 result St: N | | | | ========================================== reduce in RatPost : q2 rewrites: 18 result St: | | Q | | | | ========================================== reduce in RatPost : e1 rewrites: 10 result St: | | * | | e | | | | ========================================== reduce in RatPost : e2 rewrites: 13 result St: | * | | | | e | | | | ========================================== reduce in RatPost : e3 rewrites: 25 result St: | * | | | | e | | * | | ========================================== reduce in RatPost : e4 rewrites: 57 result St: | Q | | e | | Q | | | | ========================================== close OBJ> q Bye. awk%

6. Output for the third approach

awk% obj \|||||||||||||||||/ --- Welcome to OBJ3 --- /|||||||||||||||||\ OBJ3 version 2.04oxford built: 1994 Feb 28 Mon 15:07:40 Copyright 1988,1989,1991 SRI International 2002 Feb 25 Mon 7:51:20 OBJ> in ratpost2 ========================================== obj RatPost ========================================== open ========================================== let n0 = [ 1 ] . ========================================== let n1 = [ 2 ] n0 . ========================================== let n2 = [ 2 ] n1 . ========================================== let n3 = [ 2 ] n2 . ========================================== let n4 = [ 2 ] n3 . ========================================== let q1 = [ 6 ] n1 n2 . ========================================== let q2 = [ 6 ] n2 n4 . ========================================== let e1 = [ 5 ] [ 5 ] [ 4 ] n2 . ========================================== let e2 = [ 5 ] [ 4 ] n4 . ========================================== let e3 = [ 8 ] e2 e1 . ========================================== let e4 = [ 7 ] q1 q2 e3 . ========================================== reduce in RatPost : n4 rewrites: 10 result NatN: N (| | | |) ========================================== reduce in RatPost : q2 rewrites: 18 result Rat: (| |) Q (| | | |) ========================================== reduce in RatPost : e1 rewrites: 10 result Eq: ((| |) * (| |)) e (| | | |) ========================================== reduce in RatPost : e2 rewrites: 13 result Eq: (| * (| | | |)) e (| | | |) ========================================== reduce in RatPost : e3 rewrites: 25 result Eq: (| * (| | | |)) e ((| |) * (| |)) ========================================== reduce in RatPost : e4 rewrites: 57 result Eq: (| Q (| |)) e ((| |) Q (| | | |)) ========================================== close OBJ> q Bye. awk%


To CSE 230 homepage

Maintained by Joseph Goguen
© 2000, 2001, 2002 Joseph Goguen
Last modified: Wed Feb 27 09:52:24 PST 2002