A semantical storage operator theorem for all types
| Autor: | Christophe Raffalli |
|---|---|
| Rok vydání: | 1998 |
| Předmět: |
Pure mathematics
Logic Term (logic) Type (model theory) Translation (geometry) Set (abstract data type) Algebra Mathematics::Logic TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Operator (computer programming) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computer Science::Programming Languages Order (group theory) Gödel computer Mathematics computer.programming_language |
| Zdroj: | Annals of Pure and Applied Logic. 91:17-31 |
| ISSN: | 0168-0072 |
| DOI: | 10.1016/s0168-0072(97)00041-9 |
| Popis: | Storage operators are λ-terms which simulate call-by-value in call-by-name for a given set of terms. Krivine's storage operator theorem shows that any term of type ¬D → ¬D∗, where D∗ is the Godel translation of D, is a storage operator for the terms of type D when D is a data-type or a formula with only positive second order quantifiers. We prove that a new semantical version of Krivine's theorem is valid for every types. This also gives a simpler proof of Krivine's theorem using the properties of data-types. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect