Learn Lambda Prolog!

Programming with Higher-Order Logic

Book by Dale Miller and Gopalan Nadathur

***Content in this font is a presentation note only and will be hidden in the final version***

***Content in this font is a TODO and will be hidden in the final version***

Presentation Goals:

Introduce logic as programming via proof search and *substitution* for existentially quantified variables
Basic idea of differences between different logic programming languages
Examples of problems that can be solved with logic programming
Website as artifact for future reference, possibly extended with more explanation for learning and using the languages (chelsea.lol/pwhol)

MAIN TODO LIST:

Visual indication of which menu link is currently selected

Area for conventions?

Future: unification

Future: module system?

Arrow through notes?

Wikipedia links?

Talk about minimal vs intuitionistic logic?

Button to toggle visibility of presentation notes?

Page of definitions and links throughout page

Page with instructions on using lambda-prolog, linux, etc

Introduction

Objective:

Use (higher-order) typed logic to express relational specifications of computations and construct valid proofs of contextual queries

The first-order and higher-order distinction will be explored more later

We're used to defining functions to operate on data, e.g. a function for reversing lists that takes a list as input and returns the passed list reversed, but here we are seeing things relationally; a relation representing list reversal is between two lists, where one is the reverse of the other; usually the last argument represents the "output", but the whole expression is a formula

Example:

Encode terms of type list and predicates to define reversal
$\mathtt{reverse \; L_1 \; L_2}$ is true or false and can mean $\mathtt{L_2}$ is the reverse of $\mathtt{L_1}$

Example:

Encode and reason about other logics and languages

Approach:

Using sequent calculus, computation is goal-directed proof search, so we start with what we want to prove at the root of a proof tree

$\longrightarrow$

$\vdots$

$\dots$

$\longrightarrow$

$\vdots$

$\longrightarrow$

Contrast this view of computation with:

Computation in functional languages as reductions to a normal form
Computation in imperative languages as updates to state

The Type System

Kinds and Types

Think of a kind as the type of a type

Kind expressions are built from the following grammar:

$$ \begin{align*} \langle \textit{kind expression} \rangle ::=& \; \textit{type} \\ |& \; \textit{type} \rightarrow \langle \textit{kind expression} \rangle \end{align*} $$

Kinds are either type or some number of types with arrows between

Each type or type constructor is related to a kind expression, declared in a kind declaration:

kind	(identifier)	(kind expression).
kind	list	type -> type.

We say "list has kind type arrow type"

The example above creates a new type constructor "list" related to the kind "type -> type"

Type constructors related to kind expressions using "$\rightarrow$" allow parametric polymorphism

The constant list, when applied to a type, is parametric in that "argument" type

see page 20/21 for discussion

Types and Terms

Type expressions are built from the following grammar: $$ \begin{align*} \langle \textit{type expression} \rangle ::=& \; \langle \textit{type variable} \rangle \\ |& \; \langle \textit{type expression} \rangle \rightarrow \langle \textit{type expression} \rangle \\ |& \; \langle \textit{type constructor} \rangle \: \langle \textit{type expression} \rangle \: \ldots \: \langle \textit{type expression} \rangle \end{align*} $$

Each term or predicate symbol we want to declare is related to a type expression, declared in a type declaration:

type	(identifier)	(type expression).
type	cons	A -> list A -> list A.

We say "cons has type A -> list A -> list A"

Type expressions using type variables allow polymorphism

cons is related to the polymorphic type expression A -> list A -> list A

The constant cons is a polymorphic data constructor to be applied to an element of type A and a list with elements of type A to give a new list of elements of type A

Type expressions using "$\rightarrow$" allow value constructors for building structured data

cons can be used to build lists, given an element and a list of appropriate type

Type espressions using type constructors must be fully applied, so well-formed type expressions are related to the kind type

list, related to the kind type -> type, is not a valid type expression
list int, related to the kind type, is a type expression

Terms and Formulas

A term is typable according to the typing rules of the logic; it is either:

Variable: a fresh variable of appropriate type, either implicitly or explicitly bound by a quantifier
(see rules $\forall_R$ and $\exists_R$)
Constant: a previously declared constant with all type variables in its type instantiated
(e.g. nil of type list int)
Application: an application of a fully-applied term symbol
(e.g. cons 1 nil)
Function: a lambda-abstraction of a term variable of appropriate type over a term
(e.g. (x : list int) \ reverse (cons 1 (cons 2 nil)) x)

The type $o$ is reserved for predicates and formulas and its use is restricted for different logics (see the description of Context in Setting and Logic Comparison)

Declare the predicate reverse as

type

reverse

list A -> list A -> o.

Formulas are terms of type $o$

reverse (cons 1 (cons 2 nil)) (cons 2 (cons 1 nil)) is a formula

Setting

Sequent, $\Sigma ; \mathcal{P} \longrightarrow G$

Represents state of a computation

Compare with state in other paradigms

"Goal $G$ is provable from the program $\mathcal{P}$ given the type declarations in the signature $\Sigma$"

Note: $\rightarrow$, the function arrow, and $\longrightarrow$, the sequent arrow, are different symbols

Signature, $\Sigma$

Available constants and their associated type expressions

nil is a constant of type list A for some type A

Initially in the signature:

Math font	Concrete syntax font	Type
$\top$	tt	$o$
$\wedge$	& or ,	$o \rightarrow o \rightarrow o$
$\vee$	;	$o \rightarrow o \rightarrow o$
$\supset$	=>	$o \rightarrow o \rightarrow o$
$\Leftarrow$	:-	$o \rightarrow o \rightarrow o$
$\forall$	pi	$(A \rightarrow o) \rightarrow o$
$\exists$	sigma	$(A \rightarrow o) \rightarrow o$

Note: -> is used in place of $\rightarrow$ as the function arrow in code

The symbol \ is used as a binding operator

In the term $(f : \tau_1) \backslash (x : \tau_2) \backslash f \; x$, the variable names $f$ and $x$ are bound in the expression $f \; x$

Types of bound variables can be inferred and left out of the expression

The term $(f : \tau_1) \backslash (x : \tau_2) \backslash f \; x$ can be rewritten as $f \backslash x \backslash f \; x$

$\forall (x : T) \, F$ is shorthand for $\forall ((x : T) \, \backslash \, F)$ and $\exists (x : T) \, F$ is shorthand for $\exists ((x : T) \, \backslash \, F)$

Extend the signature using kind and type declarations to declare types, data constructors, and predicates of an application area

kind	list	type -> type.
type	nil	list A.
type	cons	A -> list A -> list A.
type	length	list A -> int -> o.

Program, $\mathcal{P}$

A set of assumed formulas representing partial definitions of predicates

length nil 0.

pi H \ pi T \ pi N \ length (cons H T) (1 + N) :- length T N.

Goal, $G$

A goal is sometimes called a query

A formula we would like to prove, assuming the formulas in $\mathcal{P}$ and using the constants declared in $\Sigma$

sigma M \ length (cons 1 (cons 2 (cons 3 nil))) M.

Unification is a process of finding substitutions for variables that simultaneously satisfy a set of equalities

Valid substitutions for existential variables found by unification represent a solution to the computation

The proof of the example above can be seen in "Search Strategy"

Horn Clauses vs Hereditary Harrop Formulas

Recall the sequent: $\Sigma ; \mathcal{P} \longrightarrow G$

Let $G$ be a syntactic category representing goals

Let $D$ be a syntactic category representing program clauses

Let $A$ be a syntactic category representing atomic formulas (formulas with no top-level logical symbol)

expand atom discussion? fully-applied constants declared in type declarations?

Horn clause grammar:

$$ \begin{align*} G ::=& \; \top \;\; | \;\; G \wedge G \;\; | \;\; G \vee G \;\; | \;\; \exists_\tau x \, G \\ D ::=& \; A \;\; | \;\; G \supset D \;\; | \;\; D \wedge D \;\; | \;\; \forall_\tau x \, D \end{align*} $$

Hereditary Harrop grammar:

$$ \begin{align*} G ::=& \; \top \;\; | \;\; G \wedge G \;\; | \;\; G \vee G \;\; | \;\; \exists_\tau x \, G \;\; | \;\; D \supset G \;\; | \;\; \forall_\tau x \, G \\ D ::=& \; A \;\; | \;\; G \supset D \;\; | \;\; D \wedge D \;\; | \;\; \forall_\tau x \, D \end{align*} $$

Hereditary Harrop goals include $D \supset G$ and $\forall_\tau x \, G$
Alternation between goals and program clauses using $\supset$

Modular programming and hypothetical reasoning:

Implication in goals allows program modification during proof search via $\supset_R$ rule

Modular programming example: Restricted scope for auxiliary predicates (see p. 125-126 of PwHOL).

type	reverse	list A -> list A -> o.
reverse L K :- pi rv \
	(rv nil K &
	(pi X \ pi N \ pi M \ rv (X :: N)) M :- rv N (X :: M))

See FOHH in "Examples" for an example using hypothetical reasoning

Generic reasoning:

Universal quantification in goals allows context modification during proof search via $\forall_R$ rule

See HOHH in "Examples" for an example using generic reasoning

Show appropriate rule when discussed

First-Order vs. Higher-Order Logic

Type Expression Order

Recall: Type expressions constructed from the following grammar (restricted in first-order): $$ \begin{align*} \langle \textit{type expression} \rangle ::=& \; \langle \textit{type var} \rangle \\ |& \; \langle \textit{type expression} \rangle \rightarrow \langle \textit{type expression} \rangle \\ |& \; \langle \textit{tyc} \rangle \: \langle \textit{type expression} \rangle \: \ldots \: \langle \textit{type expression} \rangle \end{align*} $$

*The grammar above allows higher-order types, but this will be restricted for certain sublogics

The order of type expressions is defined as: $$ \begin{align*} \textit{ord}(\tau) =& 0, \qquad\qquad \textrm{provided } \tau \textrm{ is non-functional} \\ \textit{ord}(\tau_1 \rightarrow \tau_2) =& \textit{max}(\textit{ord}(\tau_1) + 1, \textit{ord}(\tau_2)) \end{align*} $$

Informally, order is the maximum number of nested arrows

If $\mathit{ord}(T_1) = \mathit{ord}(T_2) = 0$, then

$\mathit{ord}(T_1 \rightarrow T_2) = 1$

$\mathit{ord}((T_1 \rightarrow T_2) \rightarrow T_3) = 2$

$\mathit{ord}(((T_1 \rightarrow T_2) \rightarrow T_3) \rightarrow T_4) = 3$

First-Order Restrictions:

Type expressions representing type of a term variable must have order $0$ and not be $o$

No quantification over functions or formulas in first-order

Type expression order $\leq$ 1

No functional arguments to value constructors and no function abstractions

e.g.

Sort $o$ not used in type expressions except as target type

Arguments to value constructors cannot be formulas

Type variable substitutions are expressions of order $0$ and not $o$

Otherwise terms can have order $> 1$ or represent higher-order predicates

Proof Search Strategy

The proof search process alternates between goal reduction and backchaining phases

Goal reduction:

When the top-level symbol of the goal is a logical constant, use the appropriate right-rule

$\vdots$

$\Sigma ; \mathcal{P} \longrightarrow B_1$

$\vdots$

$\Sigma ; \mathcal{P} \longrightarrow B_2$

$\wedge_R$

$\Sigma ; \mathcal{P} \longrightarrow B_1 \wedge B_2$

$\vdots$

During goal reduction, search process is independent of the context and program

(Rules visible here; describe how used; explain that or-rule ignored?)

Backchaining:

When the goal is atomic, look to the program to continue proof search:

use the decide rule to select a program clause
use either the initial rule or the backchaining rule on the chosen clause

All program clauses can be written in the form $\forall_{\tau_1} x_1 \dots \forall_{\tau_m} x_m ((A_1 \wedge \dots \wedge A_n) \supset A_0)$

When our current goal is an atom that with substitutions for variables matches the consequent of a program clause,

e.g. $\mathit{length} \; (\mathit{cons} \; 1 \; \mathit{nil}) \; 1$ is a goal that matches the consequent of clause $\forall \, \mathit{H} \; \forall \, \mathit{T} \; \forall \, \mathit{N} \; (\mathit{length} \; (\mathit{cons} \; H \; T) \; (1 + N) :- \; \mathit{length} \; T \; N)$ when $H = 1$, $T = \mathit{nil}$, and $N = 0$

use the rule backchain to change the proof state to a sequence of new states, each representing an antecedent of the previously focused formula

From above, the new goal is $\mathit{length} \; nil \; 0$

Proof of $\exists M \; \mathit{length} \; (\mathit{cons} \; 1 \; (\mathit{cons} \; 2 \; (\mathit{cons} \; 3 \; \mathit{nil}))) \; M$:

Let $P_1 = \mathit{length \; nil} \; 0$.

Let $P_2 = \forall \, \mathit{H} \; \forall \, \mathit{T} \; \forall \, \mathit{N} \; (\mathit{length} \; (\mathit{cons} \; H \; T) \; (1 + N) :- \; \mathit{length} \; T \; N)$.

Let $\mathcal{P} = \{ P_1 , P_2 \}$.

Partial walkthrough of proof:

Let the context $\Sigma$ be augmented with

nil : list A

and

cons : A -> list A -> list A

Let the program be

$\mathcal{P} =$ { length nil 0, length (cons H T) (1 + N) :- length T N},

the set of predicates defining length of a list.

Our initial goal is

sigma M \ length (cons 1 (cons 2 (cons 3 nil))) M.

We are in a goal-reduction phase.

First use $\exists_R$ to reduce the goal and get the new state

$\Sigma ; \mathcal{P} \longrightarrow$ length (cons 1 (cons 2 (cons 3 nil))) t

We have a side condition that M = t.

The new goal is atomic, so backchain choosing the second program clause,

length (cons H T) (1 + N) :- length T N,

which we will call $P_2$. The new state is

$\Sigma ; \mathcal{P} \overset{P_2}{\longrightarrow}$ length (cons 1 (cons 2 (cons 3 nil))) t

Keeping track of the side condition t = 1 + N, use the backchain rule to get the new state

$\Sigma ; \mathcal{P} \longrightarrow$ length (cons 2 (cons 3 nil)) N

Backchain two more times to get the substitution M = 3 as the solution to the query, once the system of equations of side conditions is solved.

First-Order Hereditary Harrop Formulas (FOHH)

Encoding horn clauses:

Declare propositional constants of type $o$ and write program clauses to specify relationships between the propositional variables. The implication of the object logic (FOHC) is encoded as implication in the ambient logic (FOHH).

Example from p. 78 of PwHOL.

/* Signature declarations: */
type	q, r, s, t, u	o.
/* Program definition: */
s :- r, q.
t :- q, u.
q :- r.

Proof of r => s:

$(r \wedge q) \supset s \in \mathcal{P}$

$r \in \mathcal{P}$

initial

$\Sigma ; \mathcal{P} , r \overset{r}{\longrightarrow} r$

decide

$\Sigma ; \mathcal{P} , r \longrightarrow r$

$r \in \mathcal{P}$

initial

$\Sigma ; \mathcal{P} , r \overset{r}{\longrightarrow} r$

backchain

$\Sigma ; \mathcal{P} , r \overset{r \supset q}{\longrightarrow} q$

decide

$\Sigma ; \mathcal{P} , r \longrightarrow q$

backchain

$\Sigma ; \mathcal{P} , r \overset{(r \wedge q) \supset s}{\longrightarrow} s$

decide

$\Sigma ; \mathcal{P} , r \longrightarrow s$

$\supset_R$

$\Sigma ; \mathcal{P} \longrightarrow r \supset s$

some proof explanation

Update proof above; need $r \in \mathcal{P}, r$

Higher-Order Hereditary Harrop Formulas (HOHH)

Encoding type inference for a fragment of minimal logic

Declare a kind for object logic types and types for object logic type constructors
Declare a kind for object logic expressions and types for application and abstraction and a predicate for typing
Declare a type representing object logic typing
Write program clauses to specify the type inference rules

Higher-order: The type of fun, the constant representing function abstraction, has order 2

Hereditary Harrop: The goal in the second tp_pred predicate specification has universal quantification and implication in the goal

Example modified from p. 103 of Types and Programming Languages by B. Pierce. Discussion of a similar encoding using higher-order abstract syntax can be found on p. 17 of Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax by A. Felty and A. Momigliano.

/* Signature declarations: */
kind	tp	type.
type	basetp	tp.
type	arr	tp -> tp -> tp.
kind	expr	type.
type	app	expr -> expr -> expr.
type	fun	(expr -> expr) -> expr.
type	istp	expr -> tp -> o.
/* Program definition: */
istp (app E1 E2) T1 :- istp E1 (arr T2 T1) & istp E2 T2.
istp (fun (x \ E x)) (arr T1 T2) :- pi x \ (istp x T1 => istp (E x) T2).

Example goal: sigma T \ istp (fun (f \ (fun (x \ (app f x))))) T

Answer set substitution: T = arr (arr T1 T2) (arr T1 T2)

We find that the Church numeral for 1, $\lambda f \lambda x (f \; x)$, has type $(T_1 \rightarrow T_2) \rightarrow T_1 \rightarrow T_2$

Proof of $\exists T \; \mathit{istp} \; (\mathit{fun} \; (x \; \backslash \; (\mathit{app} \; f \; x))) \; T$:

Let $P_1 = \mathit{istp} \; (\mathit{app} \; E_1 \; E_2) \; T_1$ :- $\mathit{istp} \; E_1 \; (\mathit{arr} \; T_2 \; T_1) \wedge \mathit{istp} \; E_2 \; T_2$.

Let $P_2 = \mathit{istp} \; (fun \; (x \; \backslash \; E \; x)) (\mathit{arr} \; T_1 \; T_2)$ :- $\forall x \; (\mathit{istp} \; x \; T_1 \supset \mathit{istp} \; (E \; x) \; T_2)$.

Let $P_3 = \mathit{istp} \; f \; (\mathit{arr} \; t_1 \; t_2)$

Let $\mathcal{P} = \{ P_1 , P_2 , P_3\}$

/* Signature declarations: */
kind	bintree	type -> type.
type	empty	bintree A.
type	node	A -> bintree A -> bintree A -> bintree A.
/* Program definition: */
nodeCount empty 0.
nodeCount (node V T1 T2) (1 + N1 + N2) :- nodeCount T1 N1 & nodeCount T2 N2.

/* Signature declarations: */
type	sublist	(A -> o) -> list A -> list A -> o.
type	flagged	A -> o.
type	v, w, x, y, z	A.
/* Program definition: */
sublist P (X :: L) (X :: K) :- P X, sublist P L K.
sublist P (X :: L) K :- sublist P L K.
sublist P nil nil.
flagged x, flagged y, flagged z.