Higher Order Parameterized Programming
Higher Order Parameterized Programming
First order parameterized programming has long been a key feature of the OBJ language family, and it has been
well described in several publications, including the OBJ3 manual, Introducing OBJ, and Parameterized Programming and Software
Architecture. Recent work extends this to second and higher order
parameterized programming, which allows parameterized views, parameterized
view expressions, and passing parameterized modules as parameters. Here we
give three examples which involve the encapsulation of induction using higher
order modules in various ways.
Parameterized views can be used: (1) to assert that a parameterized module
has certain properties, which are themselves parameterized; and (2) to allow a
parameterized parameter to be instantiated with a (possibly parameterized)
module. Although parameterized views were not implemented in OBJ3, they are
described in Sections 4.7 and C.8 of the OBJ3 manual, Introducing OBJ, and also in the
paper More Higher Order Programming
in OBJ, from which the first example below is taken, inspired by work
of Feng, Sakabe, and Inagaki, in a paper that is cited in More Higher Order Programming in
OBJ.
The code of the first example defines an induction scheme for the natural
numbers, and then instantiates it for proving the associativity of addition.
The module TERM
defines terms that involving addition and
variables x, y, z
over the naturals. The constant required by
NATF0
represents the induction variable, and PTERM
defines terms that may involve that variable; this parameterized module will
be the target of parameterized views. The next theory is for picking out the
two terms to be proven equal. Then goal and hypothesis modules are defined,
parameterized by the inductive constant and the terms to be proven equal. The
parameterized view ASSOCV
provides the left and right sides of
the associativity equation, using the induction variable a
from
the parameter module NATF0
. Since this variable is a parameter,
it can be instantiated in different ways for the proof. The module
IND
gives the proof structure for induction over naturals, using
the parameterized view three times, once instantiating a
to
0
for the base case, then to x
for the inductive
hypothesis, and finally to s x
for the goal of the inductive
step.
The second example is both simpler and more sophisticated, because it
passes as a parameter the parameterized module GOAL
which
specifies the two terms to be proved equal. The result proved is the familiar
formula for the sum of the first natural numbers,
1 + 2 + ... + n = n(n + 1)/2 .
The third example is another proof of the associativity of addition, this
time taking the approach of the second example, and in particular, reusing its
induction scheme. All of these examples are the result of collaboration
between Joseph Goguen and Kai Lin.
1. BOBJ Source Code for the First Induction Example
*** file: ind.obj
*** induction using higher order parameterized programming
obj TERM is sort NatTerm .
op 0 : -> NatTerm .
op s_ : NatTerm -> NatTerm .
op _+_ : NatTerm NatTerm -> NatTerm .
vars M N : NatTerm .
eq 0 + N = N .
eq s M + N = s(M + N) .
ops x y z : -> NatTerm .
let sx = s x .
endo
th NATF0 is pr TERM .
op a : -> NatTerm .
endth
obj PTERM[A :: NATF0] is ex TERM .
endo
th 2TERM[A :: NATF0] is pr PTERM[A] .
ops t1 t2 : -> NatTerm .
endth
obj GOAL[A :: NATF0, T :: 2TERM[A]] is
let goal = t1 == t2 .
endo
obj HYP[A :: NATF0, T :: 2TERM[A]] is
eq t1 = t2 .
endo
view ASSOCV[A :: NATF0] from 2TERM[A] to PTERM[A] is
op t1 to (a + (y + z)).
op t2 to ((a + y) + z).
endv
make IND is
(GOAL *(op goal to base))[(0).TERM, ASSOCV[(0).TERM]]
+ HYP[(x).TERM, ASSOCV[(x).TERM]]
+ (GOAL *(op goal to step))[(sx).TERM, ASSOCV[(sx).TERM]]
endm
red base and step . ***> should be: true
2. BOBJ Output for the First Induction Example
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.126 built: Tue Oct 30 01:45:45 PST 2001
University of California, San Diego
Tue Oct 30 10:48:20 PST 2001
BOBJ> in ind
==========================================
obj TERM
==========================================
th NATF0
==========================================
obj PTERM
==========================================
th 2TERM
==========================================
obj GOAL
==========================================
obj HYP
==========================================
view ASSOCV
==========================================
make IND
==========================================
reduce in IND : base and step
result Bool: true
rewrite time: 141ms parse time: 1ms
==========================================
***> should be: true
3. BOBJ Source Code for the Second Induction Example
***> file: /net/cs/htdocs/groups/tatami/bobj/examples/ind3.bob
obj NAT is sort Nat .
op 0 : -> Nat .
op s_ : Nat -> Nat .
op _+_ : Nat Nat -> Nat [assoc comm prec 40] .
op _*_ : Nat Nat -> Nat [assoc comm prec 20] .
vars M N : Nat .
eq 0 + M = M .
eq s M + N = s(M + N) .
eq 0 * M = 0 .
eq s M * N = M * N + N .
op sum : Nat -> Nat .
eq sum(0) = 0 .
eq sum(s M) = s M + sum(M) .
end
th TERM is pr NAT .
op x : -> Nat .
end
th GOAL[X :: TERM] is
ops l r : -> Nat .
end
th SCHEME[G :: GOAL] is
pr B is G[(0).NAT] .
pr H is G[(x).TERM] .
pr S is G[(s x).TERM] .
let base = l.B == r.B .
eq l.H = r.H .
let step = l.S == r.S .
let proof = base and step .
end
view SUMV from GOAL to GOAL is
op l to sum(x) + sum(x) .
op r to x * s(x) .
end
make SUMPROOF is SCHEME[SUMV] end
red proof .
4. BOBJ Output for the Second Induction Example
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.137 built: Mon Nov 19 13:56:29 PST 2001
University of California, San Diego
Mon Nov 19 15:23:13 PST 2001
BOBJ> in ind3
==========================================
***> file: /net/cs/htdocs/groups/tatami/bobj/examples/ind3.bob
==========================================
obj NAT
==========================================
th TERM
==========================================
th GOAL
==========================================
th SCHEME
==========================================
view SUMV
==========================================
make SUMPROOF
==========================================
reduce in SUMPROOF : proof
result Bool: true
rewrite time: 182ms parse time: 1ms
BOBJ> q
Bye.
awk%
5. BOBJ Source Code for the Third Induction Example
*** file: ind1.obj
obj TERM is sort Term .
op 0 : -> Term .
op s_ : Term -> Term .
op _+_ : Term Term -> Term .
vars M N : Term .
eq 0 + N = N .
eq s M + N = s(M + N) .
ops x y z : -> Term .
let sx = s x .
endo
th NATF0 is pr TERM .
op a : -> Term .
endth
th GOAL[A :: NATF0] is
ops l r : -> Term .
endth
obj SCHEME[G :: GOAL] is
pr B is G[(0).TERM] .
pr H is G[(x).TERM] .
pr S is G[(sx).TERM] .
let base = l.B == r.B .
eq l.H = r.H .
let step = l.S == r.S .
let proof = base and step .
endo
view ASSOCV from GOAL to GOAL is
op l to (a + (y + z)).
op r to ((a + y) + z).
endv
make ASSOCPROOF is SCHEME[ASSOCV] endm
red base and step . ***> should be: true
6. BOBJ Output for the Third Induction Example
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.137 built: Mon Nov 19 13:56:29 PST 2001
University of California, San Diego
Mon Nov 19 15:19:54 PST 2001
BOBJ> in ind1
==========================================
obj TERM
==========================================
th NATF0
==========================================
th GOAL
==========================================
obj SCHEME
==========================================
view ASSOCV
==========================================
make ASSOCPROOF
==========================================
reduce in ASSOCPROOF : base and step
result Bool: true
rewrite time: 146ms parse time: 0ms
==========================================
***> should be: true
BOBJ> q
Bye.
awk%
To BOBJ examples homepage
To Tatami project homepage
Maintained by Joseph Goguen
Last modified: Fri Dec 28 13:37:49 PST 2001