|
Descripción
|
|
|---|---|
| The Curry-Howard correspondence connects derivations in natural deduction with the lambda-calculus. Predicates are types, derivations are terms. This supports reasoning from assumptions to conclusions, but we may want to reason backwards; from the desired conclusion towards the assumptions. At intermediate stages we may have a partial derivation, with holes. This is natural in informal practice but it can be difficult to formalise. The informal act of filling holes in a partial derivation suggests a capturing substitution, since holes may occur in the scope of quantifier introduction rules. As other authors have observed, this is not immediately supported by the lambda-calculus. Also, universal quantification requires a `fresh name¿ and it is not immediately obvious what formal meaning to assign to this notion if derivations are incomplete. Further issues arise with proof-normalisation; this corresponds with lambda-calculus reduction, which can require alpha-conversion to avoid capture when beta-reducing, and it is not immediately clear how to alpha-convert a name in an incomplete derivation. We apply a one-and-a-half level technique based on nominal terms to construct a Curry- Howard correspondence for first-order logic. This features two levels of variable, but with no lambda-abstraction at the second level. Predicates are types, derivations are terms, proof-normalisation is reduction ¿ and the two levels of variable are, respectively, the assumptions and the holes of an incomplete derivation. We give notions of proof-term, typing, alpha-conversion and beta-reduction for our syntax. We prove confluence, we exhibit several admissible rules including a proof that instantiation of level two variables is type-safe ¿ this corresponds with the act of filling holes in an incomplete derivation, and can be viewed as a form of Cut-rule ¿ and we explore the connection with traditional Curry-Howard in the case that the derivation is in fact complete. Our techniques are not specifically tailored to first-order logic and the same ideas should be applicable without any essential new difficulties to similar logical systems. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
INFORMATION AND COMPUTATION |
|
ISSN
|
0890-5401 |
|
Factor de impacto JCR
|
1,225 |
|
Información de impacto
|
|
|
Volumen
|
|
|
DOI
|
|
|
Número de revista
|
|
|
Desde la página
|
230 |
|
Hasta la página
|
258 |
|
Mes
|
MARZO |
|
Ranking
|
|