An example of negation elimination in hereditary Harrop formulae

Alberto Momigliano

Consider the language of the untyped λ-calculus:

e ::= x | Λx . e | e_{1} e_{2}

We encode these expressions as terms in (labeled) hereditary Harrop formulae via the usual techniques of higher-order abstract syntax as canonical forms over the following signature:

Σ = exp : type, lam : (exp → exp) → exp, app : exp → (exp → exp)

The representation function is given by:

⌜x⌝ = x
⌜Λx . e⌝ = lam (λx:exp. ⌜e⌝)
⌜e_{1} e_{2}⌝ = app ⌜e_{1}⌝ ⌜e_{2}⌝

A term is linear if every functional subterm uses each of its arguments exactly once: in particular, we make sure that a function is linear in its first argument and then recurring on its body.

linlam : linear(lam λx . E x)
← linx(λx . E x)
← (∀x:exp. linear(x) → linear(E x)).
linapp : linear(app E_{1} E_{2})
← linear(E_{1})
← linear(E_{2}).

linxx : linx(λx . x).
linxap1 : linx(λx . app (E_{1} x) E_{2})
← linx(λx . E_{1} x).
linxap2 : linx(λx . app E_{1} (E_{2} x))
← linx(λx . E_{2} x).
linxlm : linx(λx . lam(λy . E x y))
← (∀y:exp. linx(λx . E x y)).

This is clearly a decision procedure, which can be complemented; an expression is not linear if there is some function which either does not use its argument or uses them more than once. The following is obtained via the clause complementation algorithm described in my thesis; note that ‘¬’ is not a connective but a name constructor for atoms.

¬linlam1 : ¬linear(lam λx . E x)
← ¬linx(λx . E x).
¬linlam2 : ¬linear(lam λx . E x)

← (∀x:exp. ¬linx(λx . y) ∧ linear(x) → ¬linear(E x)).

¬linapp1 : ¬linear(app E_{1} E_{2})
← ¬linear(E_{1}).
¬linapp2 : ¬linear(app E_{1} E_{2})
← ¬linear(E_{2}).

¬linxap0 : ¬linx(λx . app (E_{1} x^{1}) (E_{2} x^{1})).
¬linxap1 : ¬linx(λx . app (E_{1} x) (E_{2} x^{1}))
← ¬linx(λx . E_{1} x).
¬linxap2 : ¬linx(λx . app (E_{1} x^{1}) (E_{2} x))
← ¬linx(λx . E_{2} x).
¬linxap3 : ¬linx(λx . app (E_{1} x) (E_{2} x))
← ¬linx(λx . E_{1} x) ∧ ¬linx(λx . E_{2} x).
¬linxlm : ¬linx(λx . lam(λy . E x y))
← (∀y:exp. ¬linx(λx . y) → ¬linx(λx . E x y)).

where (E_{1} x^{1}) denotes that E_{1} must depend on x, i.e. it strict in x; the semantics of this annotation is given by the strict λ-calculus, again described in my dissertation.