This second in a series of tutorials will introduce you to functional programming the CafeOBJ way, in particular will we discuss lists and various ways to implement, use, and abuse the. We expect a running CafeOBJ interpreter being available. For a first steps tutorial, please consult this post.
Lists of natural numbers
We are adopting the following definition of list: nil is the empty list, and if x is a natural number, and L a list, then x | L is again a list. The last operation is called cons. We also assume right associativity of | so that we can drop parenthesis.
Example lists are nil, and 1 | ( 3 | ( 2 | nil ) ), which is the same as 1 | 3 | 2 | nil. Note that the last element always has to be nil, that is 1 | 3 | 2 is not a list. Also wrong parenthesing and other elements will disturb the list property.
So let us continue with the first definition of list:
mod! LIST {
pr(NAT)
[List]
op nil : -> List {constr} .
op _|_ : Nat List -> List {constr} .
}
Here we define a new module with strict (or initial) semantics, within that we use the natural numbers, define a new sort List and two operators.
Let us safe this into a file list1.cafe and see it in action:
CafeOBJ> in list1.cafe
...
CafeOBJ> open LIST .
...
%LIST> red 1 | 2 | 3 | 4 | nil .
-- reduce in %LIST : (1 | (2 | (3 | (4 | nil)))):List
(1 | (2 | (3 | (4 | nil)))):List
%LIST> close
CafeOBJ>
So we have seen that CafeOBJ can parse this expression properly.
Simple functions
Let us define some simple functions on lists, in particular length and append. The first one should return the length of the list, that is 0 for the empty list nil, and the number of other elements for other lists.
-- variables
vars N M : Nat .
vars L L1 L2 : List .
-- length
op len : List -> Nat .
eq len(nil) = 0 .
eq len(N | L) = s(len(L)) .
Here we first define some variables of type Nat and List. Some of these variables are not used by now, but will be used later! These variable declarations make equations shorter and more readable.
This is the inductive definition of len, which uses the successor function s from the natural numbers. Add these lines within the LIST module definition in list1.cafe and see it in action:
CafeOBJ> in list1.cafe
...
CafeOBJ> open LIST .
...
%LIST> red len ( 3 | 1 | 2 | 4 | 2 | nil ) .
-- reduce in %LIST : (len((3 | (1 | (2 | (4 | (2 | nil))))))):Nat
(5):NzNat
(0.000 sec for parse, 11 rewrites(0.000 sec), 16 matches)
%LIST>
We see we get the correct answer 5.
Now let us implement the append @, which takes two lists and appends the two lists. Again we take an inductive definition:
- if the first list is nil, return the second list;
- otherwise cons the first element of the first list to the append of the tail of first list with second list.
More formally in CafeOBJ code, add the following again to the list1.cafe within the module definition:
op _@_ : List List -> List
eq nil @ L2 = L2 .
eq (N | L1) @ L2 = (E | ( L1 @ L2 ) ) .
Not that we are using an infix operator for append, so that we can write: (3 | 1 | 4 | nil ) @ (13 | 12 | nil) to get the appended list. Let us see it:
CafeOBJ> in list1.cafe
...
CafeOBJ> open LIST .
...
%LIST> red (3 | 1 | 4 | nil ) @ (13 | 12 | nil) .
-- reduce in %LIST : ((3 | (1 | (4 | nil))) @ (13 | (12 | nil))):List
(3 | (1 | (4 | (13 | (12 | nil))))):List
(0.000 sec for parse, 4 rewrites(0.000 sec), 7 matches)
%LIST>
Advanced functions
Assume you want to sort a list, one of the simplest algorithm is called insert sort. The basic idea is that you have one operation insert that inserts one element into the correct place of a sorted list. And then iteratively use this function to insert each element of a unsorted list to obtain a sorted list.
As a first step let us implement insert, which takes a list, assumed to be sorted, and an element, and which returns a list where the element is inserted. Add the following code again to list1.cafe at the end of the module definition:
op insert : Nat List -> List .
eq insert( N, nil ) = ( N | nil ) .
ceq insert( N, ( M | L ) ) = ( N | M | L ) if N < M .
ceq insert( N, ( M | L ) ) = ( M | insert( N, L ) ) if N >= M .
What happens is that in line 1 we define the operator to take a natural number and a list, and returning a list. In line 2 we give the base case of the inductive definition, namely inserting an element into the empty list simply returns the one-element list, no sorting needed.
Line 3 and 4 uses conditional equations to select the correct place for the new element. If it is smaller than the first element of the list, put it at the front of the list using cons (line 3), otherwise insert it into the tail of the list.
Let us see an example:
CafeOBJ> in list1.cafe
...
CafeOBJ> open LIST .
...
%LIST> red insert( 5, 2 | 4 | 6 | nil ) .
-- reduce in %LIST : (insert(5,(2 | (4 | (6 | nil))))):List
(2 | (4 | (5 | (6 | nil)))):List
(0.000 sec for parse, 8 rewrites(0.000 sec), 15 matches)
%LIST>
So we see that the element 5 is inserted into the correct place in the list. Note that if the argument list is not sorted, the algorithm will just insert the element before the first element of the list that is smaller.
As a final step, let us define insert sort function isort, which uses the above defined insert function to insert all elements of the given list:
op isort : List -> List .
eq isort(nil) = nil .
eq isort( N | L ) = insert( N , isort(L) ) .
Here we define in line 1 the operator isort to take and return a list. Line 2 provides the base case of the inductive definition, namely that sorting the empty list returns the empty list again.
Finally, line 3 does all the tricks: If the list is not empty, that is there is a first element, then simply sort the remainder of the list and insert the first element into the right place.
Very simple and concise notation for a bit complex operation, so let us see whether it works. As usual add the above code to list1.cafe, and then we can actually see what happens with isort ( 5 | 2 | 3 | 1 | 4 | nil ):
CafeOBJ> in list1.cafe
...
CafeOBJ> open LIST .
...
%LIST> red isort ( 5 | 2 | 3 | 1 | 4 | nil ) .
-- reduce in %LIST : (isort((5 | (2 | (3 | (1 | (4 | nil))))))):List
(1 | (2 | (3 | (4 | (5 | nil))))):List
(0.000 sec for parse, 32 rewrites(0.000 sec), 58 matches)
%LIST>
Here we go, the last list is properly sorted.
For completeness, here now the full file list1.cafe
mod! LIST {
pr(NAT)
[List]
op nil : -> List {constr} .
op _|_ : Nat List -> List {constr} .
-- variables
vars N M : Nat .
vars L L1 L2 : List .
-- length of a list
op len : List -> Nat .
eq len(nil) = 0 .
eq len(N | L) = s(len(L)) .
-- append @
op _@_ : List List -> List
eq nil @ L2 = L2 .
eq (N | L1) @ L2 = (N | ( L1 @ L2 ) ) .
--
op insert : Nat List -> List .
eq insert( N , nil ) = ( N | nil ) .
ceq insert( N, ( M | L ) ) = ( N | M | L ) if N < M .
ceq insert( N, ( M | L ) ) = ( M | insert( N, L ) ) if N >= M .
--
op isort : List -> List .
eq isort(nil) = nil .
eq isort( N | L ) = insert( N , isort(L) ) .
}
Tracing
We want to finish with a short section on how to trace, that is how to see and follow the rewriting steps CafeOBJ does. The switch we are using today is set trace whole on. With this setting, CafeOBJ will inform you about the results of all rewriting steps. Let us try this first with the insert function:
CafeOBJ> in list1.cafe
...
CafeOBJ> set trace whole on
CafeOBJ> open LIST .
%LIST> red insert( 5, 2 | 4 | 6 | nil ) .
-- reduce in %LIST : (insert(5,(2 | (4 | (6 | nil))))):List
[1(cond)]: (5 < 2):Bool
--> (false):Bool
[2(cond)]: (5 >= 2):Bool
--> (true):Bool
[3]: (insert(5,(2 | (4 | (6 | nil))))):List
---> (2 | insert(5,(4 | (6 | nil)))):List
[4(cond)]: (5 < 4):Bool
--> (false):Bool
[5(cond)]: (5 >= 4):Bool
--> (true):Bool
[6]: (2 | insert(5,(4 | (6 | nil)))):List
---> (2 | (4 | insert(5,(6 | nil)))):List
[7(cond)]: (5 < 6):Bool
--> (true):Bool
[8]: (2 | (4 | insert(5,(6 | nil)))):List
---> (2 | (4 | (5 | (6 | nil)))):List
(2 | (4 | (5 | (6 | nil)))):List
(0.000 sec for parse, 8 rewrites(0.000 sec), 15 matches)
%LIST>
Reading through this one can see how CafeOBJ checks the condition on the equation, and depending on it rewrites in one or the other way. If you do now the same with isort function, then the output becomes much longer:
%LIST> red isort ( 5 | 2 | 4 | 6 | nil ) .
-- reduce in %LIST : (isort((5 | (2 | (4 | (6 | nil)))))):List
[1]: (isort((5 | (2 | (4 | (6 | nil)))))):List
---> (insert(5,isort((2 | (4 | (6 | nil)))))):List
[2]: (insert(5,isort((2 | (4 | (6 | nil)))))):List
---> (insert(5,insert(2,isort((4 | (6 | nil)))))):List
[3]: (insert(5,insert(2,isort((4 | (6 | nil)))))):List
---> (insert(5,insert(2,insert(4,isort((6 | nil)))))):List
[4]: (insert(5,insert(2,insert(4,isort((6 | nil)))))):List
---> (insert(5,insert(2,insert(4,insert(6,isort(nil)))))):List
[5]: (insert(5,insert(2,insert(4,insert(6,isort(nil)))))):List
---> (insert(5,insert(2,insert(4,insert(6,nil))))):List
[6]: (insert(5,insert(2,insert(4,insert(6,nil))))):List
---> (insert(5,insert(2,insert(4,(6 | nil))))):List
[7(cond)]: (4 < 6):Bool
--> (true):Bool
[8]: (insert(5,insert(2,insert(4,(6 | nil))))):List
---> (insert(5,insert(2,(4 | (6 | nil))))):List
[9(cond)]: (2 < 4):Bool
--> (true):Bool
[10]: (insert(5,insert(2,(4 | (6 | nil))))):List
---> (insert(5,(2 | (4 | (6 | nil))))):List
[11(cond)]: (5 < 2):Bool
--> (false):Bool
[12(cond)]: (5 >= 2):Bool
--> (true):Bool
[13]: (insert(5,(2 | (4 | (6 | nil))))):List
---> (2 | insert(5,(4 | (6 | nil)))):List
[14(cond)]: (5 < 4):Bool
--> (false):Bool
[15(cond)]: (5 >= 4):Bool
--> (true):Bool
[16]: (2 | insert(5,(4 | (6 | nil)))):List
---> (2 | (4 | insert(5,(6 | nil)))):List
[17(cond)]: (5 < 6):Bool
--> (true):Bool
[18]: (2 | (4 | insert(5,(6 | nil)))):List
---> (2 | (4 | (5 | (6 | nil)))):List
(2 | (4 | (5 | (6 | nil)))):List
(0.000 sec for parse, 18 rewrites(0.004 sec), 31 matches)
This concludes this tutorial. In one of the following tutorials we will build upon the list module developed here, and make it a parametrized module.
Pingback: Tutorial: Lists in CafeOBJ | There and back again