We consider four declarations now

kind type infixl infixrand present two more later.

localkind localIt is likely that various implementations of lambda Prolog will add various other declarations.

Each declaration associates to a token or list of tokens
some expression, either a *kind expression*, a *type expression*, or an infix priority.

**Primitive Types**

kind int type. kind real type. kind string type. kind o type.

kind -> type -> type -> type.

kind pair type -> type -> type. type pr A -> B -> pair A B.Except for the pair type, these declarations are located in some system module and need not be entered by the user.kind list type -> type. type nil list A. type :: A -> list A -> list A. infixr :: 5.

Higher priority means that binding is tighter.

Higher priority symbols appear *lower* in a parse
tree.

a + b * c = a + (b * c) 7 8+ * / / \ a * + c (wrong) / / \ b c a b

p :- N is M + N * P , X = Y :: L 1 4 7 8 2 4 5

(p :- ((N is (M + (N * P))) , (X = (Y :: L))))

On the surface, types in lambda Prolog resemble types in ML. There are important differences however.

**Minor:** Type constructors in lambda Prolog are prefix
operators while in ML they are postfix operators.

member : A -> list A -> o. member : 'a -> 'a list -> bool.

member : A -> list A -> o. member : ('a * 'a list) -> bool.

For example, both languages have the type `int`.

In ML, the intended meaning of `int` is the
collection of integers.

In lambda Prolog, the intended meaning is the set of *integer expressions*.

in ML: `5 = 2 + 3` returns `true`.

in lambda Prolog: `?- 5 = 2 + 3` fails to be provable.

type true o. type , o -> o -> o. type :-, =>, ; , & o -> o -> o.Notice that there are two conjunctions ---infixr , 2. infixr & 2. infixr ; 3. infixr :- 1. infixr => 4.

type pi, sigma (A -> o) -> o.

This duplication is adopted because:

(1) It aids readability since certain occurrence of
these connectives have different operational
reading. The convention is to use `&` and
`:-` at the top-level of program clauses and to
use `,` and `=>` at the top-level of goal
formulas.

(2) In recent work on how lambda Prolog can be ``refined''
using linear logic, the behavior of these two
conjunctions and implications diverge: in the linear
linear logic setting they are different.
*p and q => r
p and (p => q) and(q => r) => r
*

r :- p, q. r :- p, p => q, q => r. p & q => r. p & (q :- p) & (r :- q) => r.

A *signature* is an ordered list of kind, type,
and infix declarations for which the following
restrictions apply.

- If a token is given a kind declaration in this
list, that declaration must appear prior to any use of
it in a type declaration.
- If a token is given an infix declaration, that
token must be given a type declaration in the
signature prior to the infix declaration. Also, the
declared type must have at least two argument types.
- A token cannot be given two kind declarations,
two type declarations, or two infix declarations. A
token may be given both a kind and type declaration.
If such a token also has an infix declaration
associated with it, that parsing directive applies
only to the token given a type declaration.

A *Sigma* *-term of type* *\tau* is a closed
expression of type *\tau* all of whose non-logical
constants come from *Sigma*.

A *Sigma* *-formula* is a *Sigma*-term of type o.

Let *Sigma* be the following simple signature.

kind i type. type a i. type p, q i -> o.

`y\(q x => p y)` is a *Sigma + {x :
i}*-term of type `i -> o`.

`sigma y\(q x => p y)` is a *Sigma + {x :
i}*-formula.

`x\(sigma y\(q x => p y))` is a
*Sigma*-term of type `i -> o`.

`pi x\(sigma y\(q x => p y))` is a
*Sigma*-formula.
This last formula would be written in mathematical
notion as
* forall xexists y(q x => p x). *

Clausal order.

- clasual(A) = 0 provided
*A*is atomic or*top* - clasual(B1 and B2) = max(clasual(B1),clasual(B2))
- clasual(B1 or B2) = max(clasual(B1),clasual(B2))
- clasual(B1 => B2) = max(clasual(B1)+1,clasual(B2))
- clasual( forall x. B) = clasual(B)
- clasual(exists x. B) = clasual(B)

- order(A) = 0 provided
*A*is atomic or*top*} - order(B1 and B2) = max(order(B1), order(B2))
- order(B1 or B2) = max(order(B1), order(B2))
- order(B1 => B2) = max(order(B1)+1, order(B2))
- order( forall x:tau. B) = max(ord(tau)+1,order(B))
- order(exists x:tau. B) = max(ord(tau),order(B))

G ::= A | G and G

D ::= A | G => A | forall x. D

That is, goal formulas are conjunctions of atomic formulas and
program clauses are of the form
* forall x1... forall xm[A1 and... and An =>
A0]* for *m,n >= 0*. (If *m=0* then we do not write any
universal quantifiers, and if
*n=0* then we do not write the implication.)

A richer formulation is given by the following definition.

G ::= top | A | G and G | G or G | exists x. G

D ::= A | G => D | D and D | forall x. D.

Here, the connectives * top*, * or*, and *exists* are
permitted in goals and * and* and * forall* can be mixed in
definite formulas. Also, the ``head'' of a definite clause
does not have to immediately present at the top-level of a
clause: it might be buried to the right of implications and
conjunctions and under universal quantifiers.

A compact presentation of Horn clauses can be given simply as

D ::= A | A => D | forall x. D.

This is the same as the set of formulas *D* over * and*,
* =>*, and * forall* such that *order(D)* is either
0 or 1.

Lecture Directory / Module Directory / CSE360 Syllabus