 In this assignment, we will explore an alternative logic programming paradigm called relational program- ming or constraint logic programming. We will implement a variation of a constraint logic programming language called microKanren  using Haskell. We will write some interesting relations, including a relational interpreter, and use it to automatically synthesize small pieces of code given input/output examples.

Review this handout, the starter code, and the general assignment guidelines before writing any code. Also, please note that you must complete exercise 8 as a first step for this assignment.

Due date: Sunday, December 2, 10pm

### Starter code

We have divided up your work on this assignment into a few different files, with each one corresponding to one of the “Parts” described in this handout.

• Ex8.hs (from exercise 8) • A2Core.hs
• A2Reln.hs
• A2Interpreter.hs

### Prelude

We first define the idea of a relation. You are probably familiar with mathematical relations like the equality relation ==, where we say x == y if x and y are identical. We also use the language that the tuple (x, y) belongs to the equality relation. Other familiar relations include >=, <, etc.

But relations are more general than that. We can even define relations similarly to functions. Suppose we have a function f x = x + 1, with a single parameter x. Then we can define a relation fo x y, where (x, y) belongs to the relation fo if f x == y. (All of our relations will end with the letter o because Dan Friedman  thought that a superscript o looks like the upper part of a ?.)

In general, a relation can take any number of arguments, and specifies a set of n-tuples that belong to the relation. As an example, we will later define the relation appendo, which takes three arguments x, y, and xy, which is satisfied when y appended to x results in xy. We’ll talk more about defining relations later in the handout.

#### Part 0: Unification

Unification is the bread and butter of logic programming. Your first task is to complete the associated exercise, in which we implement unify and its helper functions. You will need your solution from the exercise

(contained in the file Ex8.hs) to continue.

#### Part 1: Constraint Logic Programming Core

Your work in this part should be done in A2Core.hs.
We start with the equality relation ===, which we will use like this: x === TInt 1

We use the triple equal sign to differentiate the equality relation from Haskell’s equality operator == and Haskell’s assignment operator =. Here, x is a logic variable, just like in the associated exercise. Unlike in the exercise, we won’t define logic variables manually using constructors like (TVar (LVar 0)). Instead, we will use a binary function fresh to introduce new logic variables. Here is the syntax of a relational program that uses the equality relation:

```fresh 1 (\[x] -> x === TInt 1)
```

The first argument to fresh is the number of logic variables to create. The second argument is a function that takes a list containing a new logic variable, which it calls x, and then returns the relation x === TInt 1. Note that this example uses a pattern-matching lambda function (\[x] -> …) that will raise a runtime error if called on a list of any other length.

We say that the function \[x] -> x === TInt 1 constrains the logic variable x. When we execute this program, we hope to get back possible values of x that satisfy the relation x === TInt 1.

The equality relation ===

You might guess that === has something to do with unification from Part 0, and that this constraint can be easily satisfied by setting x to TInt 1. You are absolutely right! But before we get there, we need to think long and hard about types. What should the type of === be?

As in unification, === will work with the data type Term. So, === will need to take two Terms as arguments. Like before, those terms can contain logic variables.

But what should === return? Like unification, === might succeed or fail. Perhaps the return type Maybe Substitution is sufficient?

The return type of ===: Maybe State?

Unlike in unification, we won’t work with the data type Substitution directly. Instead, we use the data type State, which is a tuple (Substitution, Int). The integer counts the number of logic variables that have been introduced so far.

Is Maybe State a good enough return type? Unfortunately, it is not. Consider this logic program:

```fresh 1 (\[x] -> (x === TInt 1) ||| (x === TInt 2))
```

In this program, ||| represents a disjunction. In English, this logic program searches for values of x that satisfies “x is equal to 1 or x is equal to 2”. Since Haskell is statically-typed, the type of (x === TInt 1) should be the same as the type of (x === TInt 1) ||| (x === TInt 2). But, in the latter case, there are two distinct substitution mappings {x: 1} and {x: 2} that would satisfy the constraints. We would like to obtain both of those mappings, but the type Maybe State would only allow one.

The return type of ===: [State]?

Perhaps the return type of === could be a list of States? We are getting closer. But why would we use a list when we can use a stream? Because Haskell is lazily evaluated, lists and streams are really one and the same. However, Haskell streams are not enough for us, because we would like to have finer control over suspending computation. You will not be implementing this “suspending computation” directly on this assignment,

but some of the provided starter code uses this, as we describe below in the section on conjunctions and disjunctions.

To be able to return multiple states, we define the polymorphic data type SusStream a in the starter code. There are three value constructors of this data type, all beginning with the character S:

• SNull is the empty stream, signifying that there are no answers,
• SCons a (SusStream a) is the stream containing one or more answers,
• SSuspended (SusStream a) is a suspended stream, used to pause computation.

So perhaps we can return a SusStream State of answers?

The return type of ===: State -> SusStream State
There is one more piece to the puzzle. Recall the type signature of unify: unify :: Term -> Term -> Substitution -> Maybe Substitution

There is a third argument, which is an accumulator that takes into account all the prior substitutions. The third argument makes it possible for unify to be called recursively. Likewise, === will need to have a third argument of type State:

```(===) :: Term -> Term -> State -> SusStream State
```

The brackets around (===) makes this relation an infix operator, so we can use syntax like x === TInt 1.

Notice also that we are only passing in two of the three arguments in the expression x === TInt 1. This is thanks to Haskell’s automatic currying! The return type of x === TInt 1 is a function State -> SusStream State, called a goal. A goal takes a state and returns a stream of states.

At this point, you should have everything you need to write ===. Since you have already written the function unify, this function should not be too hard. Hint: If the two terms unify, then you want to return an SCons. Otherwise you should return SNull.

The main function run :: (State -> SusStream State) -> [State]
Now that we have seen how a single goal like x === TInt 1 should correspond to a stream of states, we

generalize this by writing a function that takes an arbitrary goal and “solves” it.

This is the purpose of the function run, which evaluates a goal with the empty state as input, and returns a list of states. It will be the main entry point for evaluating queries, and is written for you. Here is some expected usage for this function:

```> run (fresh 1 (\[x] -> x === TInt 1))
[(fromList [(LVar 0,TInt 1)], 1)]
```

If we want just the TInt 1 (which is the “solution” for the logic variable x, the first logic variable introduced), we can use a helper function answer:

```> states = run (fresh 1 (\[x] -> (x === TInt 1)))
[TInt 1]
```

In the starter code, we have given you an implementation of the run function, but we need a few more helper functions to achieve this expected behaviour. Write the following functions:

• streamToList extracts a list of states from a SusStream. Note that this will create an infinite list if there are infinitely many substitutions that can be used to satisfy a goal.

#### Part 2: Defining New Relations

So far, we talked about the equality relation === and ways to combine relations using ||| and &&& (or disj and conj). We can now write much more interesting relations using these building blocks, by creatively using value constructors and recursion.

Your work in this part should be done in A2Reln.hs.

Our first example is a relation heado lst item, where (lst, item) belongs to the relation if the first element of the pair lst is item. The implementation of heado we have given in the starter code looks very similar to the implementation of the function t_head directly below it. The similarity is not a coincidence. Any function (f x1 x2 … xn) = y has a relational form (fo x1 x2 … xn y), and the implementation of fo will be analogous to that of f.

#### Part 3: The Relational Interpreter

In Assignment 1, you wrote an interpreter for a pattern-matching based language. You may recall that your interpreter was a function with the following arguments: (a) the environment (binding of names to values), and (b) the expression to be evaluated.

This portion of the assignment explores the relational interpreter, which is the relational analog of an interpreter. This relational interpreter will take three arguments. In addition to the expression to be evaluated and the environment bindings, the third argument will be the evaluated value of the expression.

Your work in this part should be done in A2Interpreter.hs. Language Specifications

The language is a simple one, based on the lambda calculus, but is a little clunky to write. Since our logic programming core works on Term data structures, we must build our language grammar using Term. We will support symbols, named variables, cons, car, cdr, function definitions, and function applications.

Expressions in our language will have the following grammar:

```<expr> = (TPair (TSymbol "quote") <expr>)   ; quoted data
| (TPair (TSymbol "var") (TSymbol <string>)) ; variables
```
```| (TPair (TSymbol "cons")
(TPair <expr> <expr>))
```
```| (TPair (TSymbol "car") <expr>)
| (TPair (TSymbol "cdr") <expr>)
| (TPair (TSymbol "lam")
```
```     (TPair <expr> <expr>))
| (TPair (TSymbol "app")
```
```     (TPair <expr> <expr>))
```
```  ; list construction
```
```  ; first item of a list
; rest of a list
; lambda definition
```
```; function application
```

This definition is very verbose. Your first task is to write helper functions to build these structures. Some of these wrappers are written for you. You will need to complete the definition of tcar, tcdr, tapp, tlam.

We’ll be able to use these wrappers in many places, but not when pattern matching. The Interpreter and Relational Interpreter

We have provided an interpreter eval for our language. We use the association lists defined in the previous part to represent our environment. Notice that our language follows left-to-right eager evaluation. Further, our language is lexically scoped, which means that evaluating a lambda definition results in a closure.

We have also provided a relational form of eval called evalo. This relational interpreter takes three arguments: (a) the environment (binding of names to values, which is an association list), (b) the expression to be evaluated, and (c) the output value of the evaluation.

Our definition of evalo uses lookupo, so make sure that you complete lookupo first. Since our association list allows duplicate keys, the relational interpreter will not shadow variable names properly. We will work around this by restricting our programs to only use unique variable names.

#### Conclusion

Large-scale program synthesis has been a dream of computer scientists for decades. Recently, there has been a resurgence of research in this field. We’ve included some references if you are interested in using relational programming for program synthesis. We hope this was a fun assignment! E-mail: [email protected]  微信:itcsdx 