Tutorial: First steps in CafeOBJ 3

This tutorial will guide you through starting the CafeOBJ interpreter, and some simple calculations. We will also give a very short introduction to the logic background of CafeOBJ, and the basic structure of the language.

First, please obtain the most recent CafeOBJ interpreter from the download page for your preferred operating system.

When starting the interpreter you should see something like:

-- loading standard prelude

            -- CafeOBJ system Version 1.5.2(PigNose0.99) --
                   built: 2014 Oct 30 Thu 5:39:51 GMT
                         prelude file: std.bin
                                  ***
                      2015 Feb 9 Mon 1:04:42 GMT
                            Type ? for help
                                  ***
                  -- Containing PigNose Extensions --
                                  ---
                             built on SBCL
                             1.2.4.debian
CafeOBJ> 

If you receive this prompt, you system is properly set up for the following first steps.

Simple calculations

Let us start with arithmetic, that is, calculation of functions over natural numbers. From now on we assume that you have started the interpreter already.

CafeOBJ> open NAT .
...(lots of output)...
%NAT> red 12 * 24 + 31 .

-- reduce in %NAT : ((12 * 24) + 31):NzNat
(319):NzNat
(0.000 sec for parse, 2 rewrites(0.000 sec), 2 matches)

%NAT> close
CafeOBJ> quit

Here we have done a simple computation consisting of addition and multiplication. Note that the module knows about the priority of operators, so for the above example no additional parenthesis are necessary.

Function definition

In the next step let us try to define a function that computes the square of a given number, and a function that computes the some of squares of
two numbers.

In mathematical terms that would be square(a)=a*a, and f(a,b) = a*a + b*b.

(From now on we only show the CafeOBJ code:)

open NAT .
vars A B : Nat

op square : Nat -> Nat .
eq square(A) = A * A .

op f : Nat Nat -> Nat .
eq f(A, B) = A * A + B * B .

op g : Nat Nat -> Nat .
eq g(A, B) = square(A) + square(B) .

red square(10) .
red f(3,4) .
red g(3,4) .
close

Each function definition consists of two parts: The first one op part defines the function type, that is, which type of values are taken and the type of the return value. The second part is the eq part, which provides one or more equations, or rewrite rules, how to compute the function.

Recursive functions

Recursive functions are those that are calling themselves. A simple example is the computation of the sum of all integers up to n. It can be computed by summing up all integers up to (n-1) (this is the recursive call), plus adding n. More formally, if n=0, then sum(n)=0, otherwise sum(n) = n + sum(n-1). Here we can use the p function provided by CafeOBJ, which computes the predecessor of a non-zero integer.

open NAT .
op sum : Nat -> Nat .
eq sum(0) = 0 .
ceq sum(A:Nat) = A + sum(p A) if A > 0 .
red sum(10) .
close

Let us go through this simple example line by line. Line 1 opens the natural numbers, which is as much as telling the CafeOBJ interpreter that it can use all the statements on natural numbers it knows.

Line 2 defines the arity of the sum function, as in the first example. It is a function from the natural numbers to the natural numbers. Line 3 and 4 defined the equations, or more formally the equational theory of sum, by specifying in line 3 that the sum up to 0 is 0. Line 4 contains a new construct, ceq, which is a conditional equation. It says that if A is bigger than 0, then we can compute sum(A) by computing the sum up to the predecessor of A, plus A itself.

The last line computes the sum of up integers up to 10.

Case distinction by sorts

CafeOBJ’s implementation of natural numbers distinguishes between natural numbers, and non-zero natural numbers. This allows us to rewrite the above example into simpler form, using sorts as mode of case distinction.

open NAT .
op sum : Nat -> Nat .
eq sum(0) = 0 .
eq sum(A:NzNat) = A + sum(p A) .
red sum(10) .
close

Here we see that the conditional equation in line 4 has returned to being a normal equation, but to compensate for this we have specified that the argument can only by a non-zero natural number NzNat. In-line declaration of variables like the above, where the variable name is separated from the type with a colon, are very common and effective.

Anatomy of CafeOBJ code

We conclude this tutorial with a bit of disection of what makes up CafeOBJ code.

CafeOBJ is an algebraic specification language, thus the unit of specification is an algebra, in particular an order-sorted algebra. To specify an algebra, the following information has to be given:

• signature Similar to normal algebras, a signature consists of operators and their arities. In the multi-sorted setting we are working in, this means that sorts have to be defined, and for each operator (or function) the number and sorts of the arguments and the result have to be specified.
• axioms They provide an equational theory over the (many-sorted) signature defined above. These axioms (or equations) make up the core of any algebraic specification.

We will demonstrate these concepts on a simple definition of natural numbers with successor and addition, but no comparison or subtraction:

mod! SIMPLE-NAT {
  signature {
    [ Zero NzNat < Nat ]
    op 0 : -> Zero
    op s : Nat -> NzNat
    op _+_ : Nat Nat -> Nat
  }
  axioms {
    vars N N’ : Nat
    eq 0 + N = N .
    eq s(N) + N’ = s(N + N’) .
  }
}

Line 1 begins the specification of the algebra called SIMPLE-NAT with initial semantics (indicated by the ! after mod, which can be replaced with * to indicate loose semantics). The body of the specification consists of two blocks: Lines 2-7 define the signature, lines 8-12 the axioms. In line 3 the sorts and their order are introduced by defining a partial order of sorts between brackets. In case of hidden sorts (of behavioural algebras) we use *[…]*. In the above case there are three sorts, Zero, NzZero, and Nat. The order relation expresses that the former two are a sub-sort of Nat, but does not specify a relation between themselves. Lines 4-6 give three operators, the constant 0 of sort Zero, the successor function s, and addition written in infix notation. Here the _ are the places of the arguments. The second block defines the equations by first declaring two variables of sort Nat. Axioms are introduced with the eq keyword, and the left- and right-hand side of the equation are separated by =. Thus, the above two axioms provide the default inductive definition of addition by the successor function. In the following, the signature and axioms block declaration will be dropped, as they are not necessary.

This concludes the this tutorial.