CSE 360: Lecture 3

Declarations in lambda Prolog

We consider four declarations now

kind
type
infixl
infixr

and present two more later.
localkind
local

It 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.

Built-in Types

Primitive Types

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

Types Constructors

kind  ->     type -> type -> type.

Common Definable Type Constructors

kind pair      type -> type -> type.
type pr        A -> B -> pair A B.

kind   list    type -> type.
type   nil     list A.
type   ::      A -> list A -> list A.
infixr ::      5.

Except for the pair type, these declarations are located in some system module and need not be entered by the user.

Priorities in Infix Declarations

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))))


Types in lambda Prolog

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.

Minor: Types in lambda Prolog are almost always written in curried form while in ML types are often written in uncurried form. Compare:
member : A -> list A -> o.
member : ('a * 'a list) -> bool.

Major: Types in lambda Prolog describe syntactic domains while in ML types describe semantics domains (the distinction between these domains is not always immediate).

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.

The Syntax of Formulas

type  true            o.
type  ,               o -> o -> o.
type  :-, =>, ; , &   o -> o -> o.

infixr  ,  2.
infixr  &  2.
infixr  ;  3.
infixr  :- 1.
infixr  => 4.

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

Notice that there are two conjunctions --- , & --- and two implications --- :- =>.

(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.


Signatures

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

1. 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.

2. 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.

3. 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.

Signatures are often denoted using the symbol Sigma.

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.

The Syntax of Quantification

Let Sigma be the following simple signature.

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

q x => p y is a Sigma + {x : i, y : i}-formula.

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).

Order of Formulas

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)
Combined clausal and quantificational order.
• 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))

First-Order Horn Clauses

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