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}$
list : type -> type
|
nil : list A
|
cons : A -> list A -> list A
|
Example:
Encode and reason about other logics and languages
Concerns:
-
how to define terms and predicates and declare their types
-
how order of a logic impacts computational possibilities
-
what does computation look like
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$
Contrast this view of computation with:
-
Computation in functional languages as reductions to a normal form
-
Computation in imperative languages as updates to state
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 Horn Clauses (FOHC)
Binary trees:
Specification of terms and predicate for counting the nodes in the tree.
/* 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.
|
Example goal: sigma M \ nodeCount (node 1 (node 2 (node 3 empty empty) (node 4 empty empty)) (node 5 empty empty)) M
Answer set substitution: M = 5
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}$
$\Sigma ; \mathcal{P} , r \overset{r}{\longrightarrow} r$
decide
$\Sigma ; \mathcal{P} , r \longrightarrow r$
$r \in \mathcal{P}$
$\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 Horn Clauses (HOHC)
Higher-order predicate
Filter a list by items that are flagged using a higher-order predicate. We call this predicate sublist and it takes a functional argument (order > 1) representing a polymorphic formula.
sublist definition from p. 127 of
PwHOL.
/* 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.
|
Example goal:
sigma L \ sublist flagged (cons v (cons w (cons x (cons y (cons z nil))))) L
Answer set substitution: L = cons x (cons y (cons z nil))
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
/* 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\}$