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