Author(s):
Espírito Santo, José 
Date: 2007
Persistent ID: http://hdl.handle.net/1822/8423
Origin: RepositóriUM - Universidade do Minho
Document details
Refocusing generalised normalisation
Description
When defined with general elimination/application rules, natural deduction and $\lambda$-calculus become closer to sequent calculus. In order to get real isomorphism, normalisation has to be defined in a ``multiary'' variant, in which reduction rules are necessarily non-local (reason: nomalisation, like cut-elimination, acts at the \emph{head} of applicative terms, but natural deduction focuses at the \emph{tail} of such terms). Non-local rules are bad, for instance, for the mechanization of the system. A solution is to extend natural deduction even further to a \emph{unified calculus} based on the unification of cut and general elimination. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.
When defined with general elimination/application rules, natural deduction and $\lambda$-calculus become closer to sequent calculus. In order to get real isomorphism, normalisation has to be defined in a ``multiary'' variant, in which reduction rules are necessarily non-local (reason: nomalisation, like cut-elimination, acts at the \emph{head} of applicative terms, but natural deduction focuses at the \emph{tail} of such terms). Non-local rules are bad, for instance, for the mechanization of the system. A solution is to extend natural deduction even further to a \emph{unified calculus} based on the unification of cut and general elimination. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.
Document Type
Conference Object
Language Portuguese
Language Portuguese
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||