A non-deterministic functional language.

Candidate No.  D4598

June 11, 1998

Contents

1 The Problem 3 1.1 Aim . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Union, Intersect and Converse:

the non-deterministic properties . . . . . . . . . . . . . . . . . 4 1.2.1 The Operators . . . . . . . . . . . . . . . . . . . . . . 4 1.2.2 Union . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.3 Intersection . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.4 Converse . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.3 Some examples . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 The Method 10 2.1 Compositional Logic Language . . . . . . . . . . . . . . . . . . 10 2.2 Choice of implementation language . . . . . . . . . . . . . . . 11 2.3 The Components . . . . . . . . . . . . . . . . . . . . . . . . . 12

2.3.1 Over view . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.2 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.3 Parser . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.4 The Translator . . . . . . . . . . . . . . . . . . . . . . 14 2.3.5 The Operators . . . . . . . . . . . . . . . . . . . . . . 17

3 The Solution 19 3.1 The Syntax: logexp.ml . . . . . . . . . . . . . . . . . . . . . . 19 3.2 The Lexer and Parser . . . . . . . . . . . . . . . . . . . . . . . 19

3.2.1 lexer.mll, lexer.ml . . . . . . . . . . . . . . . . . . . . . 19 3.2.2 parser.ml and parser.mly . . . . . . . . . . . . . . . . . 20

3.3 The Translator: translator.ml . . . . . . . . . . . . . . . . . . 21 3.3.1 The Translator . . . . . . . . . . . . . . . . . . . . . . 21 3.3.2 Running, Loading and Pretty Printing . . . . . . . . . 29

3.4 The Prelude: prelude.log . . . . . . . . . . . . . . . . . . . . . 30

4 Conclusions and Further study 31

A Thanks and Acknowledgement 34

B Bibliography 34

C Some running examples 34 D The code: 40

D.1 The lexer: lexer.mll . . . . . . . . . . . . . . . . . . . . . . . . 40 D.2 The Parser: parser.mly . . . . . . . . . . . . . . . . . . . . . . 40 D.3 The Translator: translator.ml . . . . . . . . . . . . . . . . . . 42 D.4 The Prelude: prelude.log . . . . . . . . . . . . . . . . . . . . . 51 D.5 The Example Programs: file1fun . . . . . . . . . . . . . . . . . 52 D.6 The start file: open.ml . . . . . . . . . . . . . . . . . . . . . . 54

1 The Problem

1.1 Aim

The non-deterministic properties of logic languages, such as Prolog, allow complex ideas to be expressed very simply although the formal structure of horn clauses can sometimes be awkward. By contrast, functional languages can be very elegant but less expressive.

The object of this project is to write a functional language with nondeterministic properties. This language should retain the elegance of functional programming with the added expressiveness of a logical language.

The three properties that I will investigate are:

i) Converse: used to run a function “backwards”. The most convenient way of implementing this feature will be to lift all restrictions on pattern matching i.e. allow any arbitrary pattern on the left hand side of function definition instead of just x:xs, n+1 etc. as in Gofer. For example a common sublist of two lists could then be found with the following function:

               com_sub :: list -> list -> list
               com_sub (XS++YS++ZS) (AS++YS++BS) = YS

ii) Union, alternatively called “or”: used to give a non-deterministic choice. This could be used to define an increasing sequence of natural number in the following way:

 increasing :: unit -> [Num]
 increasing = find_incres 0
 find_incres N = find_incres N+1 "or" N:(find_incres N+1) "or" []

iii) Intersection, alternatively called “and”: used to give non-deterministic intersect. This could be used to find an increasing common sublist of two lists in the following way:

     incr_com_sub XS YS = (com_sub XS YS) "and" increasing

This project is the first attempt to construct a language with these properties. Therefore my primary objective will be to produce a working interpreter for experimentation without considering questions of efficiency.

1.2 Union, Intersect and Converse:

the non-deterministic properties

1.2.1 The Operators

I will now set out the three main operators in more detail and introduce the notation I will use for them. These operators are:

Union or “or”, to introduce uncertainty, which I will write “}{”

Intersect or “and”, to remove uncertainty, which I will write “<>”

Converse, to run a function backwards. which I will write using pattern matching

1.2.2 Union

This allows a function or constant to be defined as the non-deterministic choice between two values, e.g. an element of a list can be the first element or one of the elements of the rest of the list:

              element (X:[])   =  X
              element (X:Y:YS) =  X }{ (element (Y:YS))

As illustrated union arguments can be functions that need to be evaluated. It would be useful if when union is given one function that terminates and one that does not or is not defined it terminates with the value of the function that terminates and does not get stuck tying to execute the other one.

   This does mean that just element (M:MS) = M }{ (element MS) would

work as a function to find an element. In the case that MS = [], element MS would be undefined, so would not be chosen. However I do not consider this a good function definition as, to a casual observer, it would seem that it has no base case and therefore is not well defined. So I would except base case to be given even when not absolutely necessary .

A constant even could be defined as any even number by observing that any even number is 0 or 2 plus another even number:

                    even    = add_twos 0
                 add_twos N = N }{ (add_twos (N+2))

1.2.3 Intersection

Intersection requires its two arguments to be the same. In Prolog X = A <> B would translate as and (A,B,X) where:

                         and (A,A,A) :-.

Intersect’s main use will be to find the intersection of two non-deterministic constants or functions. For instance, given the constants:

                           A = 1 }{ 2
                           B = 2 }{ 3

then <> can be used to find the values which they can both take, i.e.,

                           A <> B = 2

Or using even and element from 1.3.2 we can then find the even elements of a list, like so:

              even_element X = element X <> even

1.2.4 Converse

Converse can be considered as an inverse operator on a binary function, i.e. when given a binary function and an element of the range of that function it will return an element of the domain that maps onto that element of the range.

Hence converse has type (A -> B) -> (B -> A), for example, if plus (X,Y) = X+Y

then converse plus 5 equals one of the pairs: (0,5),(1,4),(2,3)...(5,0)

I will be implementing this using unrestricted pattern matching because this is a more elegant and powerful form. For example, a program to find the factors of a number could be written as:

                    factor_of  (X*Y) = X

which is little more than the rephrasing of the definition of a factor. Whereas using a converse operator this would be:

               factor_of  N =  first  (converse mult N)

1.3 Some examples

I this section I shall give some examples of the sort of things I would like to be able to write in this language. My first example is a simple logic problem. Then there is a basic parser and, finally, I give some list functions.

A simple logic problem My first problem is a logic problem, taken from Mike Spivey’s book: [3]:

Holiday homes must be designed so as to make them as pleasant as possible. They consist of placing a front door, a door into the bedroom, a bedroom window and a window in the main room. The best design will have:

• The bedroom window facing East to catch the morning sun.

• The bedroom door at right angles to the bedroom window.

• The front door adjacent to the bedroom door for privacy

• and the main room window opposite the front door for a feeling of space.

Example:

I will represent answers to this problem as a tuple: (A,B,C,D)

where A = Front door B = Bedroom door C = Main room window D = Bedroom window

We know that the bedroom window must face east, therefore:

                   rooms = (A,B,C,East)

for some suitable choice of A, B and C. The bedroom door must be adjacent to the window, so we need to define what we mean by adjacent, which we do in the function adj:

adj (North) = East  }{ West
adj (East)  = North }{ South
adj (South) = East  }{ West
adj (West)  = North }{ South

With this function we can now say where B must be:

rooms = (A,B,C,East)
        where B = adj East

The next rule we have to apply is that the front door must be adjacent to the bedroom door. We can add this to the function rooms in the same way:

rooms = (A,B,C,East)
        where A = adj B
          where B = adj East

Finally we must place the main window. This must be opposite the front door. We therefore define opposite:

opp (North) = South
opp (East)  = West
opp (West)  = East
opp (South) = North

and add the window to finish the code:

rooms = (A,B,C,East)
        where C = opp A
          where A = adj B
            where B = adj East

This example shows the appeal of this language, which is that this program was created by just going through each of the rules and encoding them. The program wrote itself with no real effort by the programmer. Of course with more complex problems this would not always be the case, and with simpler problems other languages would encode just as easily. It should be noted that, at present, local definitions have not been implemented so this program could not be run.

A very simple Parser: Now let us take this method to a more serious computing problem: that of parsing. For this example I will use the simple language:

                    expr ::= term + term | term
                      term ::= (var * var) | var
                     var  ::= x | y | z |(expr)

We need a function parse_expr that will take an expression of this language in its abstract syntax, in a list. So, taking a natural common sense view of what parse_expr should be, we get:

       parse_expr XS = (parse_plus XS) }{ (parse_term XS)

This poses the new questions: what should parse_plus and parse_term be? Using converse they have the obvious definition:

        parse_term XS = (parse_mul XS)  }{ (parse_var XS);;

and:

 parse_plus (XS ++ [plus] ++ YS)
                 = [b] ++ [add] ++ parse_term XS ++ parse_term YS ++ [d]

where I am using b and d to represent brackets. The rest of the definitions of the parser follows in the same way. So the finished code is:

   parse_expr XS = (parse_plus XS) }{ (parse_term XS);;
   parse_term XS = (parse_mul XS)  }{ (parse_var XS);;
   parse_var XS  = (parse_xyz XS)  }{ (parse_b_expr XS);;
   parse_plus (XS ++ [plus] ++ YS)
             = [b] ++ [add] ++ parse_term XS ++ parse_term YS ++ [d];;
   parse_mul ([b]++ XS ++ [mul] ++ YS ++ [d])
             = [b] ++ [times] ++ parse_var XS ++ parse_var YS ++ [d];;
   parse_xyz ([x]) = [x];;
   parse_xyz ([y]) = [y];;
   parse_xyz ([z]) = [z];;
   parse_b_expr ([b] ++ XS ++ [d]) = parse_expr XS

This example shows how the language allows the encoding of the programmer’s most basic instincts about the way a problem should be solved. This is the case even with problems of this kind which are usually thought of as difficult.

I do not suggest that this solution is the most elegant of efficient solution but I do claim that it is the most natural solution in any language and therefore would be the easiest to understand and to write for a student who had never seen the problem before.

Lists: To find an element of a list:

element (N:[])   = N
element (N:M:MS) = N }{ (element (M:MS))

or

element XS = sfold or XS

where:

   sfold f ([])   = []
   sfold f (X:XS) = (f X) ++ (fold f XS)
com_sub (XS++YS++ZS) (AS++YS++BS) = YS
init_segment (XS ++ YS) = XS
end_segment (XS ++ YS) = YS
segment XS = init_segment(end_segment XS)
interleave A ([])   = [A]
interleave A (X:XS) = (A:X:XS) }{ ([X] ++ (interleave A XS))
rotation (XS ++ YS) = YS++XS
subsequence ([])   = []
subsequence (X:XS) = (subsequence XS) }{ ([X] ++ subsequence XS)

2 The Method

To implement the non-deterministic parts of this language I would have to write a unification algorithm, produce a list of possible solutions and give a reduction stratagem; an arrangement that would in fact be very like that of existing logic languages. So, as my aim is to make a prototype version to demonstrate how such a language will work, rather than an efficient implementation for practical programming, I will translate my language into an existing logic language and then run it.

2.1 Compositional Logic Language

The logical language I will use is the compositional logic language of [1]. This language will always terminate if termination is possible because it uses a so-called “fair” selection rule. This is vital for my purpose, because I want to be sure that all well written functions in my language will terminate and as I am translating them using an algorithm, it will not always be clear what will translate to a non-terminating logic program.

For example, the definition of rotation from the last section seems to be valid but if we translate it to:

         rotation (B,A) :- append (Y,X,A), append (X,Y,B).

and then run :- rotation [1,2,3,4] Ans. in Prolog it will fail to terminate, as Prolog’s left selection rule will keep on finding Xs and Ys to make up the B without reference to the condition imposed by the list.

This is the concrete syntax of the language:

           program  ::= [function]
           function ::= expr ":-" goals | expr ":-"
           goals    ::= expr | expr,goals

and the abstract syntax is:

 program    ::= [hornclause]
 hornclause ::= (expr,[expr])
 expr       ::= Var of string | Con of string | Ap (expr,expr)

The language works by loading the logic definition in abstract syntax into a hashing table. From this, definitions are looked up when needed. What is significant for my use is that it will terminate if possible. Further detail is not necessary although it would be an area for further work.

2.2 Choice of implementation language

One of the most important questions to be answered was which language to use. My first choice was the lazy functional language: Gofer. Not only does it make it easy to express what I am doing without getting bogged down in administrative detail, but, in [2], Simon Peyton Jones has written a parser and lambda lifter for a simple functional language that could easily be adapted.

Unfortunately, this choice was wrong. In the translator it is necessary to introduce unused variables. Therefore it is necessary to keep track of which variables have been handed out already or been used by the programmer. In writing some test programs I found that the only way around this was to add an extra parameter to each function and have each function return a pair.

Such a pair would consist of the normal output of the function and a list of variables used so far. A local definition would then be needed to sort out the parts, viz.:

 buildarg :: [Argument] -> Expr -> [Lexpr]
 buildarg [] a = []
 buildarg ys (EAp (a,b)) = (buildarg (hd ys) a)++(build (tail ys)) b)

buildarg takes a list of arguments from a function and an expression in tree form and matches each element of the list with a branch of the tree and concatenates the answer. If an extra list for used variables is added the function becomes:

 buildarg ::[Var] -> [Argument] -> Expr -> ([Lexpr],[Var])
 buildarg vars [] a = ([],[])
 buildarg vars ys (EAp(a,b)) = (init_of_exp++last_of_exp, argvar++buildvar)
               where (init_of_exp,argvar  ) = buildarg vars (hd ys)   a
                     (last_of_exp,buildvar) = buildarg vars (tail ys) b

This made things rather messy and hard to follow which defeats the point of using Gofer in the first place. Therefore, I chose to switch to Caml Light: a strict functional language with assignments. In this language I could use the assignments to keep track of the variables handed out and, to save time, as a pointer to the next free variable. Also, since this language is mainly functional, it should be as easy to read and understand as Gofer.

2.3 The Components

2.3.1 Over view

I will translate the abstract syntax of my language to the abstract syntax of the logic language. This, therefore, will require a parser for my language and a translator. I will also need ways of reading and running functions. I will aim for an arrangement similar to Gofer’s scripts and sessions.

2.3.2 Syntax

I have kept my language simple. Its concrete syntax is more or less a subset of Gofer. The important additions are the binary operators }{ and <>, and that any expressions are allowed to appear as arguments.

The concrete syntax is:

toplevel ::= function | function ; toplevel
function ::= Con args "=" expr
args ::= empty | (expr) args | Var
expr ::= application
| expr binop expr
application ::= atomic
              | application atomic
atomic ::= Var | Con | Int | list | (expr)
list         ::= "[" listcontents "]"
listcontents ::= empty | expr,listcontents
binop ::= + | - | * | / | <> | }{
Int ::= number
Var ::= Capital_letter string
Con ::= small_letter   string
string ::= empty | _| letter string

I have kept the abstract syntax as close the the Compositional Logic Language as possible. For functions, I kept the notation of [2]: a triple of the function’s name, the arguments of that function and the expression itself. The only difference is that the list of arguments is now a list of expression not restricted to variables.

The abstract syntax is:

programs       ::= [function_defs]
function_defs  ::=  (Con of string, [expr], expr)
expr           ::= Con of string | Var of string | Ap (expr expr)

Numbers are implemented as constants using the set theory idea that all numbers are made up of a zero and a successor function, i.e. I have a constant zero and function succ so:

 0 = zero
 1 = succ(zero)       or Ap (Con "succ", Con "zero")
 2 = succ(succ(zero)) or Ap (Con "succ", Ap(Con "succ",Con "zero"))
 etc.

Lists are implemented similarly. With nil as the empty list and “:” or cons and a function that will join an element to the front of a list, e.g:

        [] =   nil
       [1] =  1:nil  or Ap (Ap (Con "cons", Con "1"),Con "nil")
     [1,2] = 1:2:nil or Ap (Ap (Con "cons", Con "1"),
                                Ap (Con "cons", Con"2"), Con "nil"))
           etc.

Since the user will not want to receive: Ap(Ap(cons,1),(Ap(cons,2),nil)) when they ask what [1] ++ [2] is, I have made some changes to the pretty printer of the logic language in order to print lists nicely. This has already been done for numbers.

2.3.3 Parser

In the absence of a parser written by someone else, I have written my own parser using Caml-yacc: a compiler compiler and Caml-lex: a tool for generating lexical analysers. These are very similar to the yacc and lex of C.

2.3.4 The Translator

The translation will work by first parsing the program it is given and then translating each function definition separately. I therefore need a function:

translate ::= Abstract_functional_syntax -> Abstract_logical_syntax

To help me in this I will represent function trees as spines. These are lists whose first element is the function and those following are its arguments. For example:

 com_sub (XS++YS) (map f ZS) -> [com_sub, (XS++YS), (map f ZS)]

To go between these I will use the functions spine and unspine.

An expression with no complex argument can be translated from functional to logical syntax by turning it into a spine, changing the name of the function to the appropriate logical predicate (e.g. + becomes plus) and adding an extra variable for the “output”, which I will call the answer variable from now on. Finally I will unspine it. For example:

expression which as a tree is:

   add 1 2

Becomes the spine:

       [add,1,2]

Which becomes

    [plus,1,2,Ans]

Which in turn becomes by unspining:

    plus 1 2 Ans

And in a full function, it is also necessary to carry over the answer variable, e.g.

expression which as a tree is:

f X = add X 3

which becomes:

[f,X] = [add,X,3]

which becomes:

[f,X,Ans] & { Ans = [add,X,3] }

which becomes:

f X Ans :- & {[plus,X,3,Ans]}

which becomes:

f X Ans :- plus X 3 Ans

This is simple enough when arguments are variables or constants and not more complex expressions. Logic predicates cannot be applied to other predicates directly, therefore I must read through each of the functions used in my language and pick out the applications, replacing them with new variables and making a note of the variables and expressions taken out so that I can add them later. Example:

              g X Y =  add (times X 2) (times Y 3)

In this case we must replace the add’s two arguments by variables. So, skipping some of the working, this becomes:

   g X Y A :-  where A = add (times X 2) (times Y 3)

which becomes:

   g X Y A :- plus B C A  where B = times X 2, C = times Y 3

B and C are then worked out as above, which gives:

             g X Y A :- plus B C A,mul X 2 B, mul Y 3 C .

If non-variable expressions are used as arguments they must be taken out too. When I have a variable equalling some constant on its own, I will use the id relation. One final example:

                      fac (0)   = 1
                      fac (1+N) = mul N (fac N)

The first function:

fac B A :- {where A = 0 and B = 1)}

becomes

                fac B A :- id A 0, id 1 B.

And the second becomes

       fac B A :- mul N C A and (C = fac N and B = N + 1)

which becomes:

          fac B A :- mul N C A, succ N B,  fac N C.

2.3.5 The Operators

There is now the question of how each of the operators should be translated.

Converse: As I am implementing this using unrestricted pattern matching I will simply remove the patterns from the left hand side of the function definition and introduce them as new goals.

Union: As I have said, I wish union to terminate even if one of its arguments does not. Therefore translating

               foo = bar }{ moo  as  or (bar,moo,foo) where
                         or (A,B,A) :- .
                         or (A,B,B) :- .

will not work, as this requires both arguments to be evaluated. An alternative would be to to extract the function’s arguments and translate

       foo X = (bar X) }{ (moo X)  as  or (bar,moo,X,foo)

where

                       or (F,G,X,A) :- F(X,A).
                       or (F,G,X,A) :- G(X,A).

But a definition like this might be hard to implement. For instance, in the function definition:

          foo XS = ([1,2]++XS++[3]) }{ (map inc (XS++[6]))

It is not easy to decide exactly what the two functions being applied to XS are. So I will implement union by making two version of each function definition; one for each branch of the union, e.g.

                  inc_or_dec X = (inc X) }{ (dec X)

will translate as:

                  inc_or_dec X Ans :- inc X Ans.
                  inc_or_dec X Ans :- dec X Ans.

Intersection: This is easier than Union because both its arguments must be evaluated. Therefore I can simply replace it with the logic predicate and:

                         and (A,A,A) :-.

However this would cause a problem with functions with no argument i.e. it would not be able to distinguish them from values. For example:

              even_element X = element X <> even

would translate as:

          even_element X Ans :- and even C Ans,  element X C

The easiest way to solve this problem is to give these functions a dummy variable, which is what I will do.

3 The Solution

The language is implemented in the following files:

logexp.ml, the syntax and some functions parser.mly, the parser’s source code lex.mll, the lexer translator.ml, the translator

loglex.ml }

logpar.mly } The logic language

loguse.ml } interpreter.ml }

and a Makefile which puts this together into the file:

language; the finished languages

The following sections describe what these files do.

3.1 The Syntax: logexp.ml

As the syntax of my language and the logic language is needed in the parser and the main body of the program, I have put them in the separate file; logexp.ml which can be opened when needed. This file also contains the functions needed in the parser, such as:

enter_clause : from the logic language which is used to enter logic definition into the database of the logic language.

mk_num: which translates the natural numbers used in the concrete syntax to the set theory style numbers used in the abstract syntax. This is done by a simple recursive process.

and mk_list which translates lists in a similar way to mk_num.

3.2 The Lexer and Parser

3.2.1 lexer.mll, lexer.ml

The finished lexer is in lexer.ml and is generated from lexer.mll by passing it to Caml-lex. The file lexer.mll is made up of two sections:

The first part is enclosed in {}’s and includes commands to be executed verbatim in lexer.ml. In this case, these commands are to open the parser, where the tokens used below are defined and to define an end of file marker.

The second part defines the tokens (symbols I will be using) and starts with the line:

   rule Token = parse

to define the entry point to this lexer. So the lexer is then called by lexer__token. The definition first defines what the token looks like then gives its meaning in curly brackets, e.g. for variables and constants:

  [`A`-`Z`][`a`-`z``A` -`Z``0`-`9``_`]* { VAR (get_lexeme lexbuf) }
| [`a`-`z`][`a`-`z``A` -`Z``0`-`9``_`]* { CON (get_lexeme lexbuf) }

or for the simpler symbols:

 ...
| `[`                { OPENLIST }
| `]`                { CLOSELIST }
| `+`                { PLUS }
| `-`                { MINUS }
 ...

I will not allow the user to define infix operations, so I have defined every infix symbol I wish to use here. I will then translate it in the parser rather than in the main translation algorithm, so as not to have to consider special cases.

3.2.2 parser.ml and parser.mly

Caml-yacc is a very powerful tool which almost writes the parser directly from the grammar. I do, however, have to define the tokens I am going to use and their associativity. Then it is the same as Caml-lex, in that I define what a piece of my program will look like, then give it a meaning in curly brackets, e.g:

deflist:
      def                 { [$1] }
    | def DSEMI deflist   { $1::$3 }
;

However as numbers and lists cannot be translated directly, I use the functions mk_num and mk_list from logexp as their meanings:

  | INT                    { logexp__mk_num $1 }
  | list                   { logexp__mk_list $1}

Apart from that the concrete syntax encodes directly except the binary operation which I translate here:

express:
  application              { $1 }
| express PLUS express     { EAp (EAp (ECon "plus", $1),$3) }
| express MINUS express    { EAp (EAp (ECon "minus", $1),$3) }
| express TIMES express    { EAp (EAp (ECon "mult", $1),$3) }
| express DIV express
...

3.3 The Translator: translator.ml

In this file are the translator algorithm and the machinery to run it, read programs etc.

3.3.1 The Translator

The translation algorithm is the heart of this language. It is based as closely as possible on the method I outlined in section 2.3.4. I will first give an overview of my code, then go over it a second time in more detail.

The Translation Functions: an overview The translation takes place using 6 main functions:

i) translate: This parses its input, applies breed to it then mapstranslate_line to each individual function.

ii) breed : This function reads through a program in abstract syntax and makes any function definitions with an or into two function definitions without that or. It will repeat this process until all the ors have been removed.

iii) translate_line : This translates a single function definition using the three functions below

iv) read_tho_args : This reads the the arguments (the second element of the triple) and replaces all the non-variable arguments with new variables and pairs off the new variables with the expression they represent.

v) make_goal : This takes a variable/expression pair from read_tho_args, read_tho or the original function definition and translates them into goals using read_tho and itself recursively.

vi) read_tho : This reads through a spine and like read_tho_args replaces all the arguments which are functions with new variables and pairs off the new variables with their related expressions.

The diagram opposite shows how they relate to each other.

As well as these, I have a function newvars which returns a free variable and of course other basic housekeeping functions such as spine and unspine.

The Translation functions in more detail Below I describe each function with its code and an abstract type statement.

translate:

translate :: abstract_functional_program -> abstract_logical_program
let translate =
fun
xs ->
let par_xs = (parser__Main lexer__Token (lexing__create_lexer_string xs)) in
                  map translate_line (breed par_xs)
;;

A program, a list of function definitions in concrete syntax, is translated by applying this function to it. This function first parses the list into abstract syntax then applies breed to it to get rid of the ors. Finally it maps translate_line to each function definitions.

breed:

breed ::  abstract_functional_program -> abstract_functional_program
                      |                              |
                    with or's                    without or's
let rec breed =
fun
   [] -> []
| ((a,b,c)::xs) ->
        let (exprl,flagl) = processl 1 c in
          let (exprr,flagr) = processr (1-flagl) c in
           match (flagl) with
            1 -> [(a,b,exprl)] @ (breed xs)
          | 0 -> (breed [(a,b,exprr)]) @ (breed [(a,b,exprl)]) @ (breed xs)
;;

This removes the ors by using the functions processr and processl. These functions read through the function tree and if they find an or they replace it with its right and left branch respectively. They also return a flag to say if they have found an or:

let rec processr =
fun
   0 e                          -> (e,0)
|  1 (ECon x)                   -> (ECon x,1)
|  1 (EVar x)                   -> (EVar x,1)
|  1 (EAp (EAp (ECon "or",a),b)) -> (b,0)
|  1 (EAp (a,b))                ->
        let (expra,flaga) = processr 1 a in
          let (exprb,flagb) = processr flaga b in
             (EAp(expra,exprb),flagb)
;;

processl is the same except for returning (a,0) when it finds an or. breed works by taking a function definition and applying processr to it. If this comes back without finding an or then there is nothing more to do, so we continue with the other function definitions. If we do find an or we apply processr to find the function made by choosing the other or branch. We then apply breed again to the two new function definitions we have found, as they might include more occurrences of or. Finally we then apply it to the remaining function.

translate line :

translate_line :: functional_function_def -> logical_predicate_def
let  translate_line = fun
    (name,args,expr) -> begin
    usedvar:=(map word_to_int (find_var args));num := 65;
    let v = newvar () in
let (exps_and_vars,approved_args) = read_tho_args [] [] args in
    ((unspine ([Con name] @ (approved_args) @ [v])),
                      (super_map make_goal exps_and_vars)
                                               @ (make_goal (v,expr)))
end
;;

where super_map is a map that concatenates its answers.

This, as the name suggests, translates a single function definition. It is here that we must consider how the unused variables are going to be produced, as variables can only be bound across a single function definition. I switched to Caml-light, which uses assignments, to deal with exactly this situation. So I will introduce two variables:

usedvar a pointer to type [num] num a pointer to type num

The variables my program will introduce will be A to X, then, if more are needed, they will be X1,X2...Xn... The users may not use these last ones. The use of the single alphabet letters will make programs easy to read. I will encode these variables as their ASCII numbers for A to Z and 92 + n for Xn.Therefore,

usedvar will be a list of encodings for all the variables of this type that have so far been used.

num will be a pointer to the minimum possible unused variable. This is only used to save time when finding new variables since, if we know we have handed out variables A to V, there is no point starting at A again when looking for a unused one.

I will discuss the machinery of how this works later in this section. Because it is necessary to set this up before doing anything else, translate_line starts with:

    usedvar:=(map (word_to_int.find_var) args); num := 65

where find_var picks out the variables and word_to_int encodes them.

So, once we have the machinery for generating unused variables, translate_line gets on with the job of translating the function. It generates the Hornclause in the abstract form:

(expr,[expr])

It is first necessary to read through the arguments of the function (conveniently parsed into the second element of the triple) and to replace any arguments that are not variables with unused variables. For this, I use the function read_tho_args, which returns a list of variables to be used and a list of new goals with their answer variables. I apply unspine to the function name and to the variable and the answer variables to give the first expression.

I then use make_goal with the expressions and answer variables to make the right hand side of the Hornclause.

make goal :

 makegoal :: (var  ,  expr)   ->   goal
                |        |           |
         name given to   |    the logic version
          logic output   |        of expr
                         |
              expression to be evaluated

let rec makegoal =
fun
  (a,bexpr) -> begin
  let (var_otherexprs,arg) = read_tho [] [] (super_spine bexpr) in
    [unspine (arg@[a])] @ (super_map makegoal var_otherexprs)
  end
;;

As stated above, this function takes an expression and answer variable and returns a logic expression. It works by simply adding on the answer variables to the tree:

But, in many cases, functions will have non-variable expressions as their arguments, so read_tho is used the find them and replace then with new unused variables. But read_tho takes a spine so it is necessary to apply spine to the input expression.

But there is a special case to be considered here: what if this expression is not a function? For example in the case of f x = 0. We cannot run 0 as a logic function and get 0 as the answer since 0 is not a function. What I want is the goal id 0 A. I have therefore replaced the function spine with super_spine which checks to see if the id function is needed and, if so, inserts it:

let super_spine x =
match (needid x) with
  true  -> [ECon "id"; x]
| false -> spine x
;;

where:

let rec needid =
  function
  EAp (ECon "succ",x)           -> true
| EAp ((EAp (ECon "cons",x)),y) -> true
| EAp(a,b)                      -> false
| ECon a                        -> true
| EVar a                        -> true
;;

This does have the rather unfortunate side effect of taking:

                           f (1) = 2

to

                       f X A :- id X 1,id 2 A.

not

                             f 1 2 :-.

These are however logically equivalent and nothing would be gained by my making a special case of this.

I then unspined the arguments read_tho gave me, together with the answer variable. The expressions and answer variable taken from the arguments must also be matched. This is done with a recursively call to make_goal.

read tho :

  read_tho ::= [(expr,var)] -> spine -> spine -> ([(Var,expr)],spine)
                    |            |        |                 |
     expr passed on with name    |  spine being processed   |
                         spine been processed            output
let rec read_tho a b = function
  []                        -> (a,b)
| (EVar x)::xs              -> read_tho a (b@[Var x]) xs
| (ECon x)::xs              -> read_tho a (b@[Con x]) xs
| (EAp (ECon "succ",y))::xs -> read_tho
                          a (b@[expr_to_term (EAp(ECon "succ",y))]) xs
| (EAp (x,y))::xs         -> begin
let v = newvar () in
            read_tho (a@([v,EAp(x,y)])) (b@[v])  xs
end
;;

This function reads through a list of expressions, changing them from functional to logical expressions, picking out the functions and replacing them with a variable. It must also keep track of the expressions picked out with their answer variables. I use dummy variables to store the spine which has already been read through and another to store a list of expressions extracted with their answer variables. I achieve this by pattern matching. EVar and ECon go to Var and Con. Numbers and lists are treated as constants as they do not need to be evaluated. The function expr_to_term is used to translate numbers and lists. For functions, I generate an unused variable and replace the expression with it and add the pair to the list of goals still to be made.

read tho args :

   read_tho :: [(expr,var)] -> [expr] -> [expr] -> ([(Var,expr)],[expr])
                    |            |        |                 |
     expr passed on with name    | expr to being processed  |
                         expr read so far                 output

let rec read_tho_args a b =
function
  []               -> (a,b)
| (EVar x)::xs     -> read_tho_args a (b@[Var x]) xs
| (notvar::xs)  -> begin
let newv = newvar () in
            read_tho_args (a@([newv,notvar])) (b@[newv])  xs
end
;;

This is a special version of read_tho. It is used on the arguments of a function where all non-variables must be removed. Since numbers, lists etc. indicate that pattern matching is taking place, we must add new goals to deal with each of these.

That then is the algorithm. All that remains is the generating of unused variables. Recall from above, that I have an array usedvar of coded, used, variables, num a number that is the code of the possible next free variable and I wish a new free variable to be returned by newvar.For the coding and decoding of variables I have the functions word_to_int and int_to_word. To hand out a new variable I use a while loop with !num’s membership of usedvar as a guard, adding one to num each time. Then, once I have found the code of the unused variable, I add it to usedvar, decode it, attach Var to it to make it a proper variable, and return it. This is the only part of the translator where I use the imperative features of Caml-light.

let newvar() =
while (mem !num !usedvar) do
  num := !num + 1
done
; usedvar := (!num)::!usedvar; Var (int_to_word !num)
;;

3.3.2 Running, Loading and Pretty Printing

To build the translation algorithm into a language I have added a number of features to help the reading and running of programs.

To start a session the languages must be started in Caml-light using

                      % camllight language

Some files must then be opened and the prelude loaded. This can be done by including the Caml-light file open.ml:

                 #include "open.ml";;
                 - : unit = ()
                 - : unit = ()
                 #

To read function definition as a string, use the function: read_string e.g.

#read_string "element ([X]) = X;;element (X:XS) = X }{ (element XS)";;
- : unit = ()

For larger functions it can be inconvenient to have to enter the whole thing in this way. I have therefore added read_file which will read the contents of a text file. e.g.:

read_file "file1fun";;
- : unit = ()

There is also the function read_run which will allow functions to be typed in a continuous loop until the ^C signal is given.

I have three commands for executing functions. The basic run command is exec which executes a single string by adding Ans on to the end and running the result as a logic query. Therefore, this does not allow infix operators to be used. e.g

#exec "element [1,2]";;
Ans = 1 ?
...

If just one function is wanted, this is all very well, but for long sessions it would be inconvenient to have to type in exec repeatedly. So I have written run_exec which will run a continuous loop, passing everything to exec after each return.

A useful feature point of logic programs is that they can be run specifying any of the parameters, including the one I am calling the answer variable. To do this I have added runlog() which will simply run the logic language. e.g.

#runlog();;
?- plus A B 3;
A = 0
B = 3 ?
...

I have also added a function ptrans which will translate a function then pretty print the logic equivalent.

3.4 The Prelude: prelude.log

In any language the user will quite rightly assume that some commands are provided as primitives. In my language there would be functions such as +, -, map, fold, etc. So I have given logic definitions of these in the file

prelude.log.

4 Conclusions and Further study

The aim of this project was to write a prototype non-deterministic functional language. This I have done. As languages like this have not been seen before, I also wished to demonstrate that such a language would be elegant and expressive.

Union and Intersect follow natural thought processes and their inclusion in this language allows many functions to be encoded directly, from their definitions. This includes both primitive ideas such as opposite in the first example and the more complex combinations used in the parser. Union, the only operator to have been looked at elsewhere, is the more powerful of the two, but intersect is its natural partner and also makes a significant contribution to the language’s expressiveness

Lifting the restriction on pattern matching was the most useful addition to this language. Many problems become simple when considered in this form: otherwise difficult code can be reduced to a matter of lines, sometimes even a single line, such as the common sub-list definition given in Section 1.

I hope that I have demonstrated the merits of this language and its difference from any existing language, functional or logical. Its hybrid programs have an elegance and simplicity not seen in either of these paradigms. If these features could be implemented efficiently, I believe they could become an important addition to existing declarative languages .

I have learned a lot by doing a large project like this. On the positive side, I learned much more about declarative languages and their execution: knowledge that will help me in any further investigation of this subject. I enjoyed the creative process of making a language and especially the freedom to take the project where I wanted. I also learnt how to use Caml-Yacc, Caml-Lex and L^{A}TEX, which obviously will come in useful in the future.

I also learned the necessity of careful planning what I was going to do before doing it. I wanted to get something encoded and running as soon as possible but realised subsequently it would have been better had I taken a week or two to work out in detail where my decisions would take me and the likely pitfalls. Because of this my initial choice of language was flawed, as outlined in section 2.2. I went for Gofer because it would have been possible to have adapted much of my code from [2] and it was a language I had already used and liked. However, these reasons were not directly related to solving the problem in hand and it is on that basis that I should have made my decision. When I finally changed to Caml-light I was a few weeks behind and, because there was no ready-made parser and lambda lifter, my original plan was now over ambitious. The effect was that I was unable to include a lambda lifter. Although this would have been a pleasing addition, it was by no means fundamental to my project.

I should have liked to have extended my basic language further. As well as dealing with data types, rational numbers and infix operators, I should have liked to include:

• Local definitions, as outlined in my original aim. This would be useful as suggested in section 1.4, although use of converse in arguments does partly compensate the lack of this feature.

• Some form of error checking and type checking. This would be a useful addition although, unlike the non-deterministic features, it would be nothing new. Existing type checker could easily be adapted.

• eta-conversion and composition. This would have made the code much more attracive to look at. For instance:

         segment xs = inital_segment (end_segment xs)
                             becomes
             segment = inital_segment.end_segment

Some form of type checking and changes to the logic language would be needed for this.

Working on this project raised some further matters which I believe it would be interesting to investigate:

• In any language that attempts to run specifications there will always be a degree of inefficiency. But, even given this, it is obvious that this language is very slow. Running in the Caml interpreter slows it down and so does translating directly into the logic language before running. Indeed, the language could be speeded up many times by compiling the existing code and making minor changes. A more interesting way of speeding it up would be to experiment with using a mixture of logical unification and reduction strategy with functional beta reduction. This would have to be done carefully because beta reduction could not always be applied. Perhaps if the user had to give the function and all the argument this could be achieved more easily.

• There is no way of choosing one particular element of non-deterministic output in terms of the others. For instance, I illustrated a way of finding a common sublist in section 1.2. It would be very nice to be able to find a sublist of maximum length with a max function like this:

max_length_common_sublist XS = max length (common_sublist XS)

One way of implementing this would be to return all the output in a list. But this would not have an obvious logical meaning. I believe that investigation of this would be the most interesting and useful next step.

A Thanks and Acknowledgement

I would like to thank Richard McPhee for help with using his language and the suggestions and comments he has made about this Project. His help has been both very useful and a great source of encouragement.

But my greatest thanks must go to my supervisor Oege De Moor. Without his enthusiasm and innovation this project would never have been started and without his patience and encouragement it would never have been finished.

B Bibliography

[1] Richard McPhee and Oege de Moor. Compositional Logic Programming. 1996.

[2] David Lester and Simon Peyton-Jones. Implementing Functional Languages: A Tutorial. Prentice-Hall 1992.

[3] Mike Spivey. An Introduction to Logic Programming through Prolog. Prentice-Hall 1996.

C Some running examples

Here is an example of a session in my language. The file which I load: file1fun contains the functions I have given as examples in this write up.

booth6:% camllight language
>       Caml Light version 0.7
#include "open.ml";;
- : unit = ()
- : unit = ()
#read_string "factor_of (X*Y) = X";;
- : unit = ()
#exec "factor_of 9";;
Ans = 1 ?
Ans = 3 ?
Ans = 9 ? .
yes

#read_string "com_fac X Y = (factor_of X) <> (factor_of Y)";;
- : unit = ()
#exec "com_fac 6 12";;
Ans = 1 ?
Ans = 2 ?
Ans = 3 ?
Ans = 6 ? .
yes
#read_string "com_sub (XS++YS++ZS) (AS++YS++BS) = YS";;
- : unit = ()
#exec "com_sub [1,2,3,4] [3,4,1,2,3]";;
Ans = nil ?

I will cut out repetitions of Ans = nil and blank lines.

Ans = 1:nil ?
Ans = 3:nil ?
Ans = 1:2:nil ?
Ans = 2:nil ?
Ans = 3:4:nil ?
Ans = 4:nil ?
Ans = 1:2:3:nil ?
Ans = 2:3:nil ?
Ans = 3:nil ?
no
- : unit = ()
#read_file "file1fun";;
- : unit = ()
#run_exec ();;

> parse_expr [x,plus,b,y,mul,z,d];
                                      {which is x+(y*z)}
Ans = b:add:x:b:times:y:z:d:d:nil ?.
                                      {which is (add x (times y z))}
yes
>parse_expr [b,b,x,plus,y,d,mul,b,y,plus,z,d,d]
                                   {which is ((x+y)*(y+z))}
Ans = b:times:b:add:x:y:d:b:add:y:z:d:d:nil ? .
                                   {which is (times (add x y) (add y z))}
yes
>  rotation [1,2,3,4,5];
Ans = 1:2:3:4:5:nil ?
Ans = 2:3:4:5:1:nil ?
Ans = 3:4:5:1:2:nil ?
Ans = 4:5:1:2:3:nil ?
Ans = 5:1:2:3:4:nil ?
Ans = 1:2:3:4:5:nil ?
no
> even_element [1,2,3,4,5,6];
Ans = 2 ?
Ans = 4 ?
Ans = 6 ?.
yes
> segment [1,2,3,5,7,11,13,17,19,21];
Ans = nil ?
Ans = 1:nil ?
Ans = 2:nil ?
Ans = 1:2:nil ?
Ans = 3:nil ?
Ans = 2:3:nil ?
Ans = 1:2:3:nil ?
Ans = 5:nil ?

Ans = 3:5:nil ?
Ans = 2:3:5:nil ?
Ans = 1:2:3:5:nil ?
Ans = 7:nil ?
Ans = 5:7:nil ?
Ans = 3:5:7:nil ?.
yes
> subsequence [1,2,3,5];
Ans = nil ?
Ans = 1:nil ?
Ans = 2:nil ?
Ans = 3:nil ?
Ans = 5:nil ?
Ans = 1:2:nil ?
Ans = 1:3:nil ?
Ans = 1:5:nil ?
Ans = 2:3:nil ?
Ans = 2:5:nil ?
Ans = 3:5:nil ?
Ans = 1:2:3:nil ?
Ans = 1:2:5:nil ?
Ans = 1:3:5:nil ?
Ans = 2:3:5:nil ?
Ans = 1:2:3:5:nil ?
no
> interleave 3 [1,2,4,5];
Ans = 3:1:2:4:5:nil ?
Ans = 1:3:2:4:5:nil ?
Ans = 1:2:3:4:5:nil ?
Ans = 1:2:4:3:5:nil ?
Ans = 1:2:4:5:3:nil ?
no
> F 2 3;

F = cons
Ans = 2:3 ?
F = or
Ans = 3 ?
F = or
Ans = 2 ?
F = plus
Ans = 5 ?
F = mult
Ans = 6 ?

>F 16 X;
F = cons
X = XS3
Ans = 16:XS3 ?
F = map
X = nil
Ans = nil ?
F = and
X = 16
Ans = 16 ?
F = or
X = B13
Ans = B13 ?
F = or
X = B14
Ans = 16 ?
F = minus
X = 16

Ans = 0 ?
F = minus
X = 15
Ans = 1 ?
F = minus
X = 14
Ans = 2 ?
F = minus
X = 13
Ans = 3 ?
.
.
.
.

D The code:

D.1 The lexer: lexer.mll

{
#open "parser";;
exception Eof;;
}
rule Token = parse
  [`A`-`Z`][`a`-`z``A` -`Z``0`-`9``_`]* { VAR (get_lexeme lexbuf) }
| [`a`-`z`][`a`-`z``A` -`Z``0`-`9``_`]* { CON (get_lexeme lexbuf) }
| [` ``\t``\n`]+     { Token lexbuf }
| [`0`-`9`]+         { INT (int_of_string (get_lexeme lexbuf)) }
| `[`                { OPENLIST }
| `]`                { CLOSELIST }
| `:`                { CONS }
| `,`                { COMMA }
| "++"               { APP }
| `=`                { EQUALS }
| "}{"               { OR }
| "<>"               { AND }
| ";;"               { DSEMI }
| `+`                { PLUS }
| `-`                { MINUS }
| `*`                { TIMES }
| `/`                { DIV }
| `(`                { LPAR }
| `)`                { RPAR }
| eof                { EOF }
;;

D.2 The Parser: parser.mly

%token <int> INT
%token <string> VAR
%token <string> CON
%token DSEMI COMMA OPENLIST CLOSELIST CONS APP
%token PLUS MINUS TIMES DIV
%token AND OR

%token LPAR RPAR
%token EQUALS
%token EOF
%left AND OR
%left PLUS MINUS
%left TIMES DIV
%{
#open "logexp";;
%}
%start Main, box
%type <logexp__expr> box
%type <(string * logexp__expr list * logexp__expr) list>  Main
%%
Main:
   deflist EOF            { $1 }
;
deflist:
      def                 { [$1] }
    | def DSEMI deflist   { $1::$3 }
;
def: CON pramlist EQUALS express  { ($1,$2,$4) }
;
pramlist:
    /* empty */             { [] }
    | pram pramlist         { $1::$2 }
;
pram:
  VAR                      { EVar $1 }
| LPAR express RPAR        { $2 }
;
express:
  application              { $1 }

| express PLUS express     { EAp (EAp (ECon "plus",  $1),$3) }
| express MINUS express    { EAp (EAp (ECon "minus", $1),$3) }
| express TIMES express    { EAp (EAp (ECon "mult",  $1),$3) }
| express DIV express      { EAp (EAp (ECon "div",   $1),$3) }
| express OR express       { EAp (EAp (ECon "or",    $1),$3) }
| express AND express      { EAp (EAp (ECon "and",   $1),$3) }
| express CONS express     { EAp (EAp (ECon "cons",  $1),$3) }
| express APP express      { EAp (EAp (ECon "append",$1),$3) }
;
application :
    box                    { $1 }
  | application box        { EAp ($1,$2) }
;
box :
    CON                    { ECon $1 }
  | VAR                    { EVar $1 }
  | LPAR express RPAR      { $2 }
  | INT                    { logexp__mk_num $1 }
  | list                   { logexp__mk_list $1}
;
list:
   OPENLIST listcontents CLOSELIST  { $2 }
;
listcontents:
 /* empty */                  { [] }
 | express                    { [ $1 ] }
 | express COMMA listcontents { $1::$3 }
;

D.3 The Translator: translator.ml

#open "logexp";;
(* memory *)
let usedvar = ref [];;

let num = ref 65;;

 (*------------------- generating free variables ---------------*)
let rec range n m = if n > m then [] else n :: range (n + 1) m
;;
let string_to_char str =
  map (nth_char str) (range 0 (string_length str - 1))
;;
(* word_to_int turns a representation of a variable into a number: *)
let word_to_int =
fun
  (EVar a) -> int_of_char (hd (string_to_char a))
| (ECon a) -> int_of_char (hd (string_to_char a))
|     _-> failwith "fail in word to int"
;;
(* int_to_word turns a number into a representation of a variable:
int_to_word :: int -> string *)
let int_to_word x =
if x > 91 then
    ((make_string 1 (char_of_int x))^string_of_int (x-91))
else
    (make_string 1 (char_of_int x)
;;
let newvar() =
while (mem !num !usedvar) do
  num := !num + 1
done
; usedvar := (!num)::!usedvar; Var (int_to_word !num)
;;

let rec (find_var : logexp__expr list -> logexp__expr list) =

  fun
 ((EVar b)::xs) -> EVar b::(find_var xs)
|  (b::xs)      -> find_var xs
|     []        -> []
;;
(*----------------------------------------------------------*)

(*------------------- house keeping functions --------------*)
let (force_type : 'a -> ((string*logexp__expr list * logexp__expr) list )) =
fun
x -> x
;;
let rec (expr_to_term : logexp__expr -> logexp__term) =
fun
  (EVar a) -> Var a
| (EAp  (a,b)) -> Ap  (expr_to_term a,expr_to_term b)
| (ECon a) -> Con a
;;
let var = fun
  x -> Var x
;;
let rec super_map =
fun
  f  []  -> []
| f (x::xs) -> f(x) @ (super_map f xs)
;;
let rec spine =
  fun
  (EAp(a,b)) -> spine a @ [b]
|  (ECon a)  -> [ECon a]
|  (EVar a)  -> [EVar a]
;;

let rec needid =
  function
  EAp (ECon "succ",x)           -> true
| EAp ((EAp (ECon "cons",x)),y) -> true
| EAp(a,b)                      -> false
| ECon a                        -> true
| EVar a                        -> true
;;
(* Super_Spine :: expr -> spine *)
let super_spine x =
match (needid x) with
  true  -> [ECon "id"; x]
| false -> spine x
;;
let rec last =
function
  x::y::xs -> last (y::xs)
|   y::[]  -> y
|    _-> failwith "lasting empty list"
;;
let rec first =
function
    x::y::xs -> x::(first (y::xs))
|    y::[]   -> []
|     []     -> []
;;
(* unspine :: spine -> term *)
let rec unspine =
function
   x::y::xs -> Ap (unspine (first (x::y::xs)), last (y::xs))
|   y::[]   -> y
|     _-> failwith "unspining emptylist";;

(* ------------------------------------------------------- *)

(*-------------------- the translation --------------------*)
let rec processl =
fun
   0 e                          -> (e,0)
|  1 (ECon x)                   -> (ECon x,1)
|  1 (EVar x)                   -> (EVar x,1)
|  1 (EAp (EAp (ECon "or",a),b)) -> (a,0)
|  1 (EAp (a,b))                ->
        let (expra,flaga) = processl 1 a in
          let (exprb,flagb) = processl flaga b in
             (EAp(expra,exprb),flagb)
;;
let rec processr =
fun
   0 e                          -> (e,0)
|  1 (ECon x)                   -> (ECon x,1)
|  1 (EVar x)                   -> (EVar x,1)
|  1 (EAp (EAp (ECon "or",a),b)) -> (b,0)
|  1 (EAp (a,b))                ->
        let (expra,flaga) = processr 1 a in
          let (exprb,flagb) = processr flaga b in
             (EAp(expra,exprb),flagb)
;;
let rec breed =
fun
   [] -> []
| ((a,b,c)::xs) ->
        let (exprl,flagl) = processl 1 c in
          let (exprr,flagr) = processr (1-flagl) c in
           match (flagl) with
            1 -> [(a,b,exprl)] @ (breed xs)
          | 0 -> (breed [(a,b,exprr)]) @ (breed [(a,b,exprl)]) @ (breed xs)
;;

(* read_tho reads through the spine of the expression to be translated
and returns the translation and a list of further expr's to be translated
with their alloted name:

   read_tho :: [(expr,var)] -> spine -> spine -> ([(Var,expr)],spine)
                    |            |        |                 |
     expr passed on with name    |  spine being processed   |
                         spine been processed            output *)
let rec read_tho a b =
function
  []                                  -> (a,b)
| (EVar x)::xs                        -> read_tho a (b@[Var x]) xs
| (ECon x)::xs                        -> read_tho a (b@[Con x]) xs
| (EAp (ECon "succ",y))::xs           -> read_tho a
                         (b@[expr_to_term (EAp(ECon "succ",y))]) xs
| (EAp ((EAp (ECon "cons",x)),y))::xs -> read_tho a
                         (b@[expr_to_term (EAp ((EAp (ECon "cons",x)),y))]) xs
| (EAp (x,y))::xs                     -> begin
   let v = newvar () in
          read_tho (a@([v,EAp(x,y)])) (b@[v])  xs
end
;;
(* make goal takes a variable and an expression and returns a list of
terms that evaluate the expression to the variable:
makegoal :: (var  ,  expr)   ->   goal
              |        |           |
       name given to   |    the logic version
        logic ouptut   |        of expr
                       |
             expression to be evaluated
*)
let rec makegoal =
fun
  (a,bexpr) -> begin
  let (var_otherexprs,arg) = read_tho [] [] (super_spine bexpr) in

    [unspine (arg@[a])] @ (super_map makegoal var_otherexprs)
  end
;;

(* read_tho_args reads through the list of arguments of the function
 and returns the list with all non-variables replaced with new variables.
and a list of those expressions paired with their newvar's:

   read_tho :: [(expr,var)] -> [expr] -> [expr] -> ([(Var,expr)],[expr])
                    |            |        |                 |
     expr passed on with name    | expr to being processed  |
                         expr read so far                 output
*)
let rec read_tho_args a b =
function
  []               -> (a,b)
| (EVar x)::xs     -> read_tho_args a (b@[Var x]) xs
| (notvar::xs)  -> begin
let newv = newvar () in
            read_tho_args (a@([newv,notvar])) (b@[newv])  xs
end
;;
(* translate_line translates a function super combinator to a horn clause:
translate_line :: supercombin -> clause *)
let  translate_line = fun
    (name,args,expr) -> begin
    usedvar:=(map word_to_int (find_var args));num := 65;
    let v = newvar () in
        let (exps_and_vars,approved_args) = read_tho_args [] [] args in
            ((unspine ([Con name] @ (approved_args) @ [v])),
                      (super_map makegoal exps_and_vars) @ (makegoal (v,expr)))
        end
;;

(* translate resets the memory, reads the used varible and applies
translate_line to each line of code:
translate :: Funprog -> Logprog *)
let translate =
fun
xs ->
let par_xs = (parser__Main lexer__Token (lexing__create_lexer_string xs)) in
                  map translate_line (breed par_xs)
;;
let translate_file =
fun
file ->
let par_xs = (parser__Main lexer__Token (lexing__create_lexer_channel
                                         (open_in  file))) in
                 map translate_line (breed par_xs)
;;
(*------------------------------------------------------------*)

(*----------------------------pretty printer------------------*)
let rec (pprint_term : term -> string) =
function
  Var a    -> a
| Con "zero" -> "0"
| Con a    -> a
| Ap (Con "succ",x) -> string_of_int (1 + int_of_string (pprint_term x))
| Ap ((Ap (Con "cons",x)),y) -> (pprint_term x) ^":" ^(pprint_term y)
| Ap (a,b) -> (pprint_term a) ^" " ^(pprint_term b)
;;
let rec (pprint_terms : term list -> string)   =
function
    []       -> ""
| (x::[])    -> pprint_term x

| (x::y::xs) -> (pprint_term x) ^", " ^(pprint_terms (y::xs))
;;
let rec (pprint: clause list -> string) =
fun
      []      -> ""
| ((a,b)::xs) -> ((pprint_term a) ^" :- " ^pprint_terms b
                                                 ^"\n" ^(pprint xs))
;;
let ptrans xs =print_string (pprint (translate xs));;

(* ------------------- running & reading programs ------------------*)
let rec read =
fun
    []   -> ()
| (x::xs) -> logexp__enter_clause x;read xs
;;
let read_string xs = read (translate xs)
;;
let run_read () =
        while true do
            print_string "<";
            let input = read_line () in
            read_string input
        done
;;
let read_file xs = read (translate_file xs)
;;
let runlog() = loguse__run (interpreter__eval  (interpreter__bfs
                                                      interpreter__stack));;
let exec = function xs ->
  let lexbuf = lexing__create_lexer_string (xs^" Ans ;") in
      let result = logpar__query loglex__token lexbuf in

      ((interpreter__eval  (interpreter__bfs interpreter__stack)) result)
;;
let run_exec () =
    let lexbuf = lexing__create_lexer_channel std_in in
        while true do
            print_string"> ";
            flush std_out ;
            (try
             let result = logpar__funquery loglex__token lexbuf in
            ((interpreter__eval  (interpreter__bfs interpreter__stack)) result)
             with parsing__Parse_error -> print_string "syntax error");
    print_newline();
    flush std_out
 done
;;

D.4 The Prelude: prelude.log

and A A A :- ;
id X X :- ;
plus zero A A :- ;
plus (succ K) X (succ A) :- plus K X A ;
minus A B C :- plus C B A ;
mult zero X zero  :- ;
mult (succ N) X A :- mult N X B, plus X B A ;
div A B C :- mult C B A;
map A nil nil :- ;
map A (B:BS) (C:CS) :- A B C,map A BS CS;
cons X XS (X:XS) :- ;

append nil C C   :-;
append X:A B X:C :- append A B C;
map Y X:XS C:D :- Y X C, map Y XS D;
map Y nil nil :- ;
sfold Y X:nil X :-;
sfold Y X:U:XS  A :- sfold Y (U:XS) C,Y X C A;
or A B A :- ;
or A B B :- ;

D.5 The Example Programs: file1fun

Some basic functions:

g A B C = A C;;
h A B = g A B B;;
triand X Y Z = X<>(Y<>Z);;
trior A B C = A}{(B}{C);;
inc X = X + 1;;
dec X = X - 1;;
even X     = add_twos 0;;
odd  X     = add_two 1;;
add_twos N = N }{ (add_twos (N+2));;
incordec X = (inc X) }{ (dec X);;
factor_of  (X*Y) = X;;
com_fac X Y = (factor_of X) <> (factor_of Y)

List functions

hd (X:XS) = X;;
element ([X]) = X;;
element (X:XS) = X }{ (element XS);;

foldelement XS = sfold or XS;;
com_sub (XS++YS++ZS) (AS++YS++BS) = YS;;
increasing  X = find_incres 0;;
find_incres N = (find_incres N+1) }{ ([N]++(find_incres(N+1))) }{ [];;
incr_com_sub XS YS = (com_sub XS YS) <> increasing X;;
even_element X = element X <> even X;;
odd_element  X = element X <> odd  X;;
inital_segment (XS ++ YS) = XS;;
end_segment (XS ++ YS) = YS;;
segment XS = initaly_segment (end_segment XS);;
rotation (XS ++ YS) = YS ++ XS;;
interleave A ([]) = [A];;
interleave A (X:XS) = (A:X:XS) }{ ([X] ++ (interleave A XS));;
subsequence ([])     = [];;
subsequence (X:XS) = (subsequence XS) }{ ([X] ++ subsequence XS);;

The parser

parse_expr XS = (parse_plus XS) }{ (parse_term XS);;
parse_term XS = (parse_mul XS)  }{ (parse_var XS);;
parse_var XS  = (parse_xyz XS)  }{ (parse_b_expr XS);;
parse_plus (XS ++ [plus] ++ YS) = [b] ++ [add] ++ parse_term XS
                                 ++ parse_term YS ++ [d];;
parse_mul ([b]++ XS ++ [mul] ++ YS ++ [d]) = [b] ++ [times]
                                 ++ parse_var XS ++ parse_var YS ++ [d];;
parse_xyz ([x]) = [x];;
parse_xyz ([y]) = [y];;
parse_xyz ([z]) = [z];;

parse_b_expr ([b] ++ XS ++ [d]) = parse_expr XS

D.6 The start file: open.ml

(* a start up file for the language*)
# open "logexp";;
# open "loguse";;
# open "interpreter";;
# open "translator";;
read_database "prelude.log";;