Loading...
Please wait, while we are loading the content...
Similar Documents
Curry-howard Isomorphism and Intuitionistic Linear Logic
| Content Provider | Semantic Scholar |
|---|---|
| Author | Roversi, Luca |
| Copyright Year | 1996 |
| Abstract | The notion of Curry-Howard Isomorphism (CHI) was originally introduced for formalizing to which extent the computational behavior of the typed-calculus (t) is joined at the semantics of the natural deduction for Intuitionistic Logic (IL). The introduction of the Intuitionistic Linear Logic (ILL) reened the semantics of the logical operators of IL. This raised the problem of studying to which extent the reenement of IL by ILL reeects on t. A method for doing that is to adapt CHI for IL to ILL. The solution to the problem is not trivial: it does not clearly exist any natural deduction which can be taken as the natural deduction for ILL because of the presence of a modality in ILL. We give our solution to the problem of nding the CHI for ILL. We introduce a natural deduction`N for ILL and a functional language N hN; !i such that the terms of N encode the deductions of`N, and ! simulates the normalization steps of`N on N. In doing that, we pay particular attention to write a N which eeectively reenes t , computationally speaking. A measure for assessing the reenement is the number of commuting conversions (CC) in !. CC represent a computational noise which, however, can not be forgotten. Indeed, CC have a basic computational meaning: they allow to extract the main computational steps from the, possibly too much involved, syntax of N. Hence, the less CC the better. However, if some CC exist in !, we can not forget them when proving properties on N, because of their basic computational meaning. It results that N globally is a good reenement of t while preserving the same expressiveness. This for various motivations. ! has fewer CC than the most robust proposal of CHI for ILL. ! is strongly normalizable, is Church-Rosser, and enjoys the subject reduction property. Moreover, both strong normalizability and the Church-Rosser property are proved in full details on the whole !, namely also on CC. 1 Finally, looking for a CHI for ILL with as little CC as possible yields a pleasant side eeect, which is a further improvement w.r.t. the previous proposals: the terms of N which type is the unity of the tensor gain a non trivial computational behavior. Because of its results and the technical details it contains, we look at this work as a deep overview of the problems which arise when extending CHI from … |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://iml.univ-mrs.fr/~rover/PAPERS/mscs96sub.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
