Qute: A Prolog/Lisp Type Language for Logic Programming

1. Symbolic Expression

1.1. definition of sexp

Symbolic expressions (sexps, for short) are con­ structed by the following clauses:

1. 0 is a sexp.
2. If s and t are sexps then snoc(s, t) is a sexp.
3. If s and t are sexps and at least one of them is not 0 then cons(s, t) is a sexp.

All the sexps are constructed only by means of the iterated applications of the above three clauses, and sexps constructed differently are distinct. We denote the set of all the sexps by S. Note that snoc is a total function on SxS while cons is partial since it is undefined for the argument (0, 0) . We make cons total by stipulating that cons(O, 0) = 0. We also put snoc(O, 0) = 1.

We denote the image of the function cons by M and that of snoc by A, so that we have two bijective functions:

Moreover, we have S = MU A and Mn A=¢; i.e., S satisfies the domain equation

Elements in M are called molecules and those in A are called atoms . By the above discussion, we can define total functions car and cdr on S by the equations

1.2. dot notation and list notation

We introduce dot notation and list notation as notations for sexps. A sexp is also called a list when it is written in dot notation or list notation.

A list which begins with ( is a cons list and a list which begins with [ is a snoc list. (. x ) is a cons list and [. x ] is a snoc list, though they denote the same sexp.

1.3. name

Let L be the set of ASCII graphic characters. We define a function p : L-A by using 7 bit ASCII codes. We explain by examples.

Note that the ASCII code of 'a' is 1100001 in binary.

A name is a string of alphanumeric characters whose length is longer than 1 and which begins with a lowercase.

A name denotes a sexp as follows:

Let n = /i · · · lk be a name, then n denotes

2. The Lisp-part of Qute

The top level read routine of Qute reads in an expression and processes it. An expression is either a Lisp expression or a Prolog expression. A Lisp (Pro­ Jog) expression will be processed by the Lisp (Prolog, resp.) part of Qute. We will explain the Lisp-part of Qute in this section. Evaluation mechanism of Lisp expressions in Qute mostly follows that of usual Lisp. However, our treatment of variables and function appli­ cations radically differs from usual Lisp.

We give some examples in 2.1, give informal explanation of eva/ in 2.2-2.6 and summarize definition of eva/ in 2.7.

2.1. examples

• (Ll) 0; =0
• (L2) [apple, orange]; = [apple, orange]
• (L3) > cons(X, Y) = (X . Y); cons defined
• (L4) cons(apple, orange); = (apple . orange)
• (LS) > snoc(X, Y) = [X. Y]; snoc defined

(L6) ·[X, cons(apple, orange)];

= [X, cons(apple, orange)]

• (L7) '[consOeft, right), X, \IY, '/snoc(left, right)]; = [consOeft, right), X, /Y, '[left . right]]
• (L8) > car((X. Y)) = X; car defined
• (L9) > cdr((X. Y)) = Y; cdr defined
• (LlO) car(snocOeft, right)); =left
• (Lll) > atom(Z = (X. Y)) = eq(Z, [X. Y]); atom defined
• (L12) eq(apple, orange); = 1
• (L13) eq(apple, apple); =0
• (L14) atom(snoc(apple, orange)); =0
• (L15) > append(X = (X1 . X2), Y) = Cond[ eq(X, 0) -> Y, 0 -> [X1. append(X2, Y)]];
• append defined
• (L16) append([aa, bb], Icc, dd, eel); = [aa, bb, cc, dd, eel
• (L17) > apply(F, X):= ('APPLY, [F. X]); apply defined
• (L18) apply(cons, [lisp, prolog]); Oisp . prolog)
• (L19) > and(. x = (x1 . x2)) := 'Cond[ eq('/x, 0) -> 0, /x1 - > And[. /x2]];
• and defined (L20) And[eq(aa, aa), 0]; =0

2.2. constant and special sexp

A molecule whose car-part is is called a special sexp. We use V AR, QUOTE, QQUOTE, ESC, EV AL respectively to denote the above atoms. A sexp which does not contain a special sexp as its sub-sexp is called a constant sexp or simply a constant.

We now explain the function eva! that is used to evaluate Lisp expressions. The function eva! is defined so that it preserves cons and snoc for non-special sexps and hence it becomes an identity function on constants. Therefore, we can make use of snoc (and cons which satisfies (r3)) as a pattern constructor. This advantage comes from the fact that we have two constructors snoc and cons.

• (rl) eva/(0) = 0

The expressions (Ll), (L2) in 2.1 are evaluated by these rules. Note that a name is a constant.

We explain evaluation rules for special sexps in the following.

2.3. variable and environment

A special sexp (VAR . x) is called a variable. We introduce a syntax sugaring for a variable. A single lowercase character followed by a string of digits or a nonempty string of alphanumeric characters which begins with an uppercase character denotes a variable. Let the string be /1 · · · ln- It denotes

Example 2.1.

The value of a variable is determined relative to an environment . An environment is a list of pairs of a variable and its value. It is created when a function or a macro is called.

Besides this environment, there is a global environment, though we do not go into details in this paper. If a variable is not found in an environment, a global environment is searched. A global environment is preserved even after evaluation.

2.4. quote and quasi-quote

For a sexp t, each of't, 't, \tand/t denotes a spe­ cial sexp (QUOTE . t), (QQUOTE . t), (ESC. t) and (EV AL . t) respectively. We say t is in the scope of ', ·, \ and I respectively. ' and · plays a similar role in eva! as that in usual Lisp. ' plays the role of quote.

In the scope of ', a special sexp loses its special mean­ ing. · plays the role of backquote in Maclisp, but our · is not a read-macro.

• (r 5) eva!( t) = qeval(t)
• (r6) qeva/(0) = 0
• (r7) qeva!([x . y]) = [qeval(x). qeva!(y)]
• (r8) qeval( (x . y)) = (qeval(x) . qevat(y))

In the scope of ·, only I and \ have a special meaning. I evaluates a sexp in its scope and \ plays the role of quotation. For examples, see (L6), (L 7), (L19) . Note that quasi-quotation is useful if we want to suspend evaluation of applications.

2.5. definition of function and macro

A function definition is of the form

where june is a name, fml is a formal parameter which is a cons list and body is a sexp. Similarly, a macro definition is of the form

where mac is a name. We cannot associate a function and a macro to the same name. For examples, see (L3), (L8), (L9), (Lll), (LIS), (L17), (Ll9).

A formal parameter is defined as follows:

• (i) a variable is a formal parameter.
• (ii) 0 is a formal parameter.
• (iii) if f 1 and f 2 are formal parameters, so are (/I . h) and [fl . hl.

In a formal parameter, / 1 = h denotes [f 1 · hl.

2.6. apply

A special sexp (APPLY, x) is called an applica­ tion. We introduce syntax sugarings for an application. They are

where fun is a name, Fun is a nonempty string of alphanumeric characters whose length is longer than 1 and which begins with an uppercase character and arg; is a sexp. Fun is distinguished syntactically from a vari­ able by the following '['.

• (1), (2) denotes respectively

where fun ' is a name obtained by replacing the leading uppercase character of Fun by the corresponding lower­ case character.

Example 2.2.

cons(apple, orange) = (APPLY, (cons . [apple, orange])) Cons[apple, orange] = (APPLY, [cons, apple, orange]) o

1. and (2) are evaluated by the following rules. (rll) eval(fun (argh · · · , arg 11 ))

Note that in (rll) eva/ also plays the role of evlis in ordinary Lisp because of the rules (rl), (r2). Whether an argument list is evaluated or not is decided not by a function or macro but by the form of a function or macro call.

apply(fun, argO is computed as follows. If fun is an atom other than eq or cond, it is regarded as a func­ tion or macro name and its definition is searched. If found, a new environment is created by the following rules from the argument list argl and the formal param­ eter fml of the definition.

pairup(O, argO = [] pairup(v, argO = [[ v . argl]] where v is a variable pairup((fl . f2), (arg/1 . arg/2)) = append(pairup(fl, arg/1), pairup(f2, argi2JJ pairup((/1 . f2), [arg/1 . argi2JJ = append(pairup(fl, arg/1), pairup(f2, argi2JJ pairup([fl . f2l, argO

= append(pairup(fl, argO, pairup(f2, arg/))

where append concatenates two lists.

Example 2.3.

Note that a formal parameter is used as a skeleton that is matched with the argument list and that a formal parameter matches any sexp because of the totality of car and cdr.

If fun is a function, its body is evaluated under the new environment.

Example 2.4.

See (L3) and (L4). cons(apple, orange) is evaluated as follows:

Evaluating the argument list [apple, orange] results in [apple, orange] . The formal parameter of cons is (X, Y) and the body is (X . Y). Pairup of (X, Y) and [apple, orange] creates a new environment

Under this environment, (X . Y) is evaluated and results in

If fun is a macro, its body is evaluated under the new environment and the result is evaluated again under the environment that was current when the macro was called.

Example 2.5.

See (L17) and (L18). apply(cons, [lisp, pro log]) is evaluated as follows:

Evaluating the argument list [cons, [lisp, prolog]] results in [cons, [lisp, prolog]]. The formal parameter of apply is (F, X) and the body is ('APPLY, [F . X]). Pairup of (F, X) and [cons, [lisp, prolog]] creates a new environment

Under this environment, ('APPLY, [F . X]) is evaluated and results in

This sexp, i.e., Cons[lisp, prolog], is evaluated under the previous environment yielding the result Oisp . pro­ Jog). o

Qute has two built-in functions eq and conq. eq returns 0 if its two arguments are equal, 1 otherwise. The definition of cond follows that of usual Lisp, except that 0 represents truth and other sexps falsity. We have a syntax sugaring for an argument of cond. That is,

Example 2.6.

See (L19) and (L20). And [eq (aa, aa), 0] is evaluated as follows:

The argument of And is not evaluated. Pairup creates an environment

Under this environment, the body of and is evaluated and the result is

This result is evaluated again. As eva/( eq (' [eq (aa, aa) , OJ, 0)) = 1 and eval(eq(aa, aa)) = 0, And(O] is evaluated. And[O] is evaluated similarly and the result is 0. o

In addition to a function and macro call, Qute also has a lambda expression, which we explain in 2.7.

2. 7. summary

We summarize the definition of eva/ in this sec­ tion. Here we define eva! as a function from SxS to S, that is, eval(x, env) = y means that evaluating x under the environment env results in y .

eval(x, env) = if x = 0 then 0 elif atom(x) then snodeval(car(x), env), eval(cdr(x), env)) elif car(x) = V AR then get(x, env) elif car(x) = APPLY then if mo!e(cdr(x)) then if atom(appl(x)) then appf)'(/n(x), arg(x), env) else apply(/n(x), eval(arg(x), env), env) fi else true(value(x), prd(x), !vars(x), env) fi elif car(x) =QUOTE then cdr(x) elif car(x) = QQUOTE then qeval(cdr(x), env) else cons(eval(car(x), env), eva!(cdr(x), env)) fi

(For the explanation of true, see section 4.)

qeval(x, env)

= if x = 0 then 0 elif atom(x) then snoc(qeva!(car(x), env), qeval(cdr(x), env)) elif car(x) = ESC then cdr(x)

elif car(x) = EV AL then eval(cdr(x), env)

else cons(qeval(car(x), env), qeval(cdr(x), env)) fi where appl is cadr, fn is caadr, arg is cdadr, value is cadr, prd is caddr and lvars is cadddr.

get(v, env) = if v = var(env) then va!(env) else get(v, rest(env)) fi

where var is caar, val is cdar and rest is cdr.

apply(!, arg, env) = if atom(/) then iff= eq then eq(car(arg), cadr(arg)) elif f = cond then evcon(arg, env) elif june(/) then eval(body(/), pairup(formai(!J, arg)) elif macro(/) then eva!(eval(body(!J, pairup(formal(!J, arg)), env) fi

else eval(bdy(!J, append(pairup(fmi(!J, arg), env))) fi

where func(f) and macro(f) decides whether f is a function or a macro, body(f) is the body of a definition off, formal(f) is the formal parameter, bdy is cadr and f ml is car. (else-part corresponds to lambda expression.)

evcon(cls, env) = if cis = [] then 1 elif eva!(prem(cls), env) = 0 then eva!(ant(cls), env) else evcon(rest(cls), env) fi

where prem is caar and ant is cadar.

This describes only the pure part of eva/. Qute has a built-in function 'set' which can change the environ­ ment. (We omit the explanation in this paper.)

3. The Prolog-part of Qute

The Prolog-part of Qute is similar to an ordinary Prolog, but there is an important difference, i.e., the argument list of the predicate and the parameter list of the assertion are evaluated before they are unified with the assertions.

We give examples in 3.1, explain syntax of Qute in 3.2 and mechanism of unification in 3.3, 3.4.

3.1. examples

(Pl) + cons I X, Y, (X. Y); cons defined (P2) - cons[apple, orange, X]; X = (afple . orange) (P3) + cadr X, Y - eq[Y, car(cdr(X))]; cadr defined (P4) - caddcons (left, (right)), Xl; X= right (PS) + append1 IO, Y, y I [X1 . X2], Y, [X1 . Z2] - append1 [X2, Y, Z2]; append1 defined (P6) - appendl[[aa, bb], X, [aa, bb, cc, ddll; X= [cc, dd] (P7) + append2 I X, Y, append (X, Y); append2 defined (P8) - append2[[prolog, lisp], [qutel, X]; X = [prolog, lisp, qute]

3.2. definition of predicate

A predicate is of the form prd arglist where prd is a name and arglist is a snoc list. Its denotation is [prd . arglist ]. prd is called the predicate name of the predicate and arglist is called the argument list of the predicate.

A predicate definition (assertion) is of the form

+ prd I param1 body 1 I param2 body2 I param 11 body 11

where prd is a name, param; is of the form

where p( is a sexp, and body; is empty or of the form

where predicate/ is a predicate.

The corresponding Marseille notation is

+prd[paramd-predicatel- · · · -predicatet'; +prd[param 11 ]-predicate 11 1 - · · ·-predicate;;"';

We call [param;l a parameter list of the assertion. A goal is of the form

- predicate 1 - predicate2 · · · - predicatem;

where predicate; is a predicate.

3.3. variable and its value

First, we define the notion of free variable . The following function vars(f) is used to define the set of free variables in f.

vars(!J = iff = 0 then ¢ elif f = [f 1 . hl then vars (f 1) U vars (h) elif f = (VAR. t) then If} elif f =fun (arg!> · · · , arg 11 ) then vars<larg!> · · · , arg 11 ]} elif f = Fun [arg!> · · · , a%1 then¢ elif f = Epsilon (val; body) then vars(body}- vars(va/) elif f = 't then ¢ _ elif f = 't then qvars(t) elif f = (fl . h) then vars(f 1) U vars(h) fi

(For simplicity, we omit the case of lambda expres­ sion.)

qvars(!J = iff = 0 then ¢ elif f = [f 1 . f 2l then qvars(f 1J U qvars(f 2J elif f = \t then¢ elif f = / t then vars(t) elif f = (fl . h) then qvars(f1) U qvars(h) fi

When a sexp f is evaluated, it is necessary to know the values of the free variables in f . However, the intended meaning of a free variable in a predicate is an unknown sexp which may be known after evalua­ tion. We introduce the notion of an undefined value Cit is an imaginary element outside of S) . We suppose that each free variable has a different undefined value.

3.4. unification

Before evaluating the predicates in a goal, an environment which is a list of pairs of a free variable and an undefined value is set up. Before an unification is made with a predicate definition, an environment is set up similarly, using free variables in the parameter and the body of the predicate definition. An undefined value plays the role of a 'variable' in unification.

Example 3.1.

creates an environment

before evaluation, where undfj is an undefined value. Evaluating [ [prolog, lisp], [qute , X] results in

According to the definition of append) in (PS), the first parameter list [0, Y, Y] is evaluated first and its result is [0, und.h, undhl. This is not unifiable with (1). So the second parameter list [[XI . X2l, Y, [XI . Zll is evaluated and its result

is unified with (1). At this time, the environment is

and undf 1 is instantiated to [undh . undf 6]. In this way, execution goes on. After execution, the first environment is instantiated to

Since no restriction is imposed on the parameters of an assertion, they may contain any special sexp as is seen in (P7) . Unification with such an assertion goes like the following.

Example 3.2.

(P8) is executed under the definition (P7), where append is a function defined in (LIS) . [[pro log, lisp], [qutel, X] is evaluated with the result

A parameter list [X, Y, append (X, Y)] of (P7) is evaluated and its result is

with the condition

That is, since we cannot evaluate append(X, Y) with free variables X and Y, we assume that its value is undf 4 and impose the above condition. (1) and (2) are unified and as a result undefined values are instan­ tiated, i.e., undh = [prolog, lisp], undh = [qute] and undf 4 = undf l · The condition is instantiated to undf 1 = append([prolog, lisp], [qute]) and it is checked. append([prolog, lisp], [qute]) is evaluated and undf 1 is instantiated to [prolog, lisp, qute]. D

4. Connecting Lisp and Prolog

One of the most important features of Qute is that the Prolog-part can be called from the Lisp-part. It is a mechanism similar to Hilbert's epsilon symbol, that is, a mechanism to find a value which makes a certain predicate to hold.

4.1. examples

• (El) > append3 (X, Y) = Epsilon(V; append3[X, Y, V]); append3 defined

• ' append3 defined (E3) append3 ( [ljsp, pro log], [qute]) ;
• = [lisp, prolog, qutel (E4) > append4(X, Y) = Epsilon(V; append4[X, Y, V]); append4 defined
• (ES) + append4 I[],Y, Y I [x . X], Y, [x . append4 (X, Y) 1 append4 defined

memb~r defined

• (E7) Epsilon (x; membedx, [apple, orange]]);

=apple

(E8) - eq[orange,

Epsilon (x; membedx, [apple, orange]])];

yes

4.2. epsilon expression

A special sexp (APPLY . [val, prds, vars]) is called an epsilon expression where val is a sexp, prds is a predicate or a cons list of predicates (i.e., conjunction of predicates) and vars is a snoc list of variables that are local in the epsilon expression. We introduce a syn­ tax sugaring for an epsilon expression. It is

where val and body are sexps. It denotes

where vars is the snoc list of the free variables in val. According to the definition of eva/ in 2.7,

= true(va/, body, vars, env)

It is computed as follows. A new environment E is set up by appending to the head of the current environ­ ment env a list consisting of pairs of a free variable in vars and an undefined value. body is executed by the Prolog-part under this environment E with the result that the environment is instantiated to an environment £' that makes body true . According to the formal specification of Qute, any £ ' that makes body true is accepted, but the actual implementation finds E' in a depth-first way. Then val is evaluated under the instantiated environment E' and the result is the value of (APPLY . [val, body, vars]). When £ ' is created a marker to this frame is also made, so that a later back­ track will return to this point.

Epsilon expression is therefore a multi-valued function, however only one value is returned at a time and further values may be obtained by using backtrack.

Example 4.1.

(E3) is evaluated under the definitions (El), (E2). append3 is called and the environment

is created by pairup. Epsilon expression which is the body of append3 is evaluated. First, a new environ­ ment

is created. A goal append3[X, Y, V] is executed under this environment according to the definition (E2). The environment is instantiated to

[[V. [lisp, prolog, qute]], [X . [lisp, prolog]],

and V is evaluated under this environment with the result [lisp, prolog, qutel. It is the value of the epsilon expression and of append3([lisp, prolog], [quteD. 0

Example 4.2.

(E6) defines an ordinary membership relation on a list. In (E7), the Lisp-part of Qute sets up an environ­ ment

and calls the Prolog-part. The Prolog-part tries to find an instance of E that makes member[x, [apple, orage]] true. The following two instances of E both give a correct instance:

However, the actual implementation does a depth-first search and returns E 1 as a new environment. The Lisp-part evaluates x in this environment and returns apple as the value of (E7).

In executing (E8), the two arguments of the predi­ cate eq are evaluated first. The second argument, which is the · same epsilon expression as (E7) , is evaluated similarly as above and apple is returned as its value. Since orange and apple are not 'eq' (equal), a backtrack occurs. This forces Qute to find a second value of the epsilon expression and the value orange :

will be returned this time. Since orange and orange are 'eq', 'yes' is returned as the answer to the question (E8) . o

5. Conclusions and Future Plans

We have shown that it is possible to amalgamate Prolog and Lisp in a natural way. A comparison of the evaluation of a Qute predicate with that of an atomic formula in a first order language will make this natural­ ness clear. Consider a first order language that includes:

• a binary predicate symbol < (for less than),

a binary function symbol + (for plus) and

constants for natural numbers

with their usual interpretations. Then the truth value of the atomic formula

is evaluated as follows. First evaluating the terms 2+ 3 and 6, we get 5 and 6. Then by the meaning of < we see that 5 is less than 6, which implies the truth of the formula in question. The evaluation in Qute is com­ pletely analogous. With appropriate definitions of "less_ than" and "plus", the question:

is evaluated by Qute resulting in the answer "yes".

According to this analogy, the evaluation of a sexp by the Lisp part of Qute corresponds to the evaluation of a term. Here, an epsilon expression corresponds to Hilbert's e-term.

We have defined the semantics of Qute informally in this paper. We wish to give a formal definition of Qute in a forthcoming paper. (See also Sakurai[2].) This will be done as follows. First, we will define a for­ mal intuitionistic theory of symbolic expressions called SA which is proof theoretically equivalent to Heyting's arithmetic HA. It will then become possible to define Qute within SA. Moreover, to mechanize these processes, we will implement a proof checking system for SA using Qute. In this way, we will be able to for­ mally reason about the properties of Qute within Qute itself.