Talk:Harrop formula

Harrop v System F

The section is about the statement "proofs of Harrop formulae correspond to terms in System F". Can someone give a reference for this assertion, please? I can't find one. Thanks. ComputScientist (talk) 14:11, 7 May 2009 (UTC)

There's one reference given. I'll try to dig out some more. Radagast3 (talk) 22:41, 7 May 2009 (UTC)

Thanks, I can find no mention of Harrop in the Proofs and Types book. (The section is currently baffling me. One problem I have is that the types of System F correspond to formulas of second order propositional logic, whereas the Harrop formulas are predicate logic.) ComputScientist (talk) 07:30, 8 May 2009 (UTC)

I see what you mean. Proofs and Types uses the concept, but not the word. Coquand may be a better reference. And you put your finger on an oversimplification with regards to 1st order vs 2nd order quantifiers. I've reworded a bit, but I'm not sure if that's enough. I don't want to oversimplify too much, yet I don't want to drown the article in technical detail either. I think using System F illustrates the basic idea -- why Harrop formulae are important -- fairly well, but perhaps there is a better way. Radagast3 (talk) 09:09, 8 May 2009 (UTC)

Hmm. 20 months on and I still don't understand this section. I don't understand the content nor the point that is trying to be made. Perhaps the idea was to explain Harrop's result from the point of view of propositions-as-types? but then (a) has this appeared in print somewhere?; (b) I expect dependent type theory is the right language, not System F?

Unfortunately Radagast seems to have disappeared. I've moved the section to this talk page, below; do revert me if you disagree. ComputScientist (talk) 07:18, 18 January 2011 (UTC)

Harrop formulae and lambda calculus

If Harrop formulae are taken as types, as in the Curry–Howard correspondence, constructive proofs of the formulae correspond to terms in some form of higher-order lambda calculus, such as System F, which has universally quantified types. We can make three definitions, which turn falsity, conjunction, and negation into derived concepts:

• $\bot \equiv \forall A.A$:

• $A\wedge B\equiv \forall C.(A\rightarrow B\rightarrow C)\rightarrow C$

• $\neg A\equiv A\rightarrow \bot$

The key to the correspondence is the proof of the remaining two kinds of formulae. Implication is proved with a lambda-term, which corresponds to assuming the antecedent, labelling this assumption with a variable, and then proving the consequent:

$\lambda x^{F}.e^{A}:F\rightarrow A$ where $e$ is a term (proof) of type $A$ (possibly containing the variable $x$ of type $F$, which may include disjunction or existential quantification)

The reason that Harrop formulae allow disjunction and existential quantification in the antecedent and not in the consequent is that the former corresponds merely to an assumption, while the latter corresponds to something that must be proved constructively. Universal quantification is proved with a higher-order lambda-term:

$\Lambda C.e^{A}:\forall C.A$ where $e$ is a term (proof) of type $A$

A similar approach can be used with the first-order quantification in Heyting arithmetic. Combining the two above cases, it can be seen that conjunction can be proved by:

$\Lambda C.\lambda f^{A\rightarrow B\rightarrow C}.fe_{1}^{A}e_{2}^{B}:\forall C.(A\rightarrow B\rightarrow C)\rightarrow C$

where $e_{1}$ is a term of type $A$ and $e_{2}$ is a term of type $B$. In other words, conjunction is proved by a pair of terms, corresponding to a pair of proofs. Other versions of typed lambda calculus take conjunction and pairing to be primitive, rather than derived, constructs, so that simply:

$(e_{1}^{A},e_{2}^{B}):A\wedge B$

System F also includes constructive ways of proving $A\vee B$, but being constructive, these cannot prove propositions such as $P\vee \neg P$. Restricting attention to Harrop formulae means this is no longer a limitation.

Where Harrop formulae are provable, finding the lambda term which acts as a proof can be done by a fairly simple search process, exploring the type-correct lambda-terms in normal form (all lambda-terms in System F can be rewritten to normal form).

References