Differential interaction nets
| Autor: | Thomas Ehrhard, Laurent Regnier |
|---|---|
| Přispěvatelé: | Institut de mathématiques de Luminy (IML), Centre National de la Recherche Scientifique (CNRS)-Université de la Méditerranée - Aix-Marseille 2, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Université de la Méditerranée - Aix-Marseille 2-Centre National de la Recherche Scientifique (CNRS) |
| Rok vydání: | 2006 |
| Předmět: |
Normalization (statistics)
Pure mathematics Correctness General Computer Science 0102 computer and information sciences proof nets 01 natural sciences Curry–Howard correspondence Theoretical Computer Science Proof calculus Tensor (intrinsic definition) Computer Science::Logic in Computer Science linear logic Calculus 0101 mathematics Algebraic number computer.programming_language Mathematics Discrete mathematics Geometry of interaction interaction nets Noncommutative logic 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Interaction nets Differential calculus lambda-calculus Differential lambda-calculus Linear logic Lambda-calculus with multiplicities Algebra Formalism (philosophy of mathematics) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics differential calculus TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Lambda calculus ACM F.3.2 computer Differential (mathematics) Resource lambda-calculus Computer Science(all) |
| Zdroj: | Theoretical Computer Science Theoretical Computer Science, Elsevier, 2006, 364 (2), pp.166-195. ⟨10.1016/j.tcs.2006.08.003⟩ Theoretical Computer Science, 2006, 364 (2), pp.166-195. ⟨10.1016/j.tcs.2006.08.003⟩ |
| ISSN: | 0304-3975 1879-2294 |
| DOI: | 10.1016/j.tcs.2006.08.003 |
| Popis: | 30 pages; International audience; We introduce interaction nets for a fragment of the differential lambda-calculus and exhibit in this framework a new symmetry between the "of course" and the "why not" modalities of linear logic, which is completely similar to the symmetry between the "tensor" and "par" connectives of linear logic. We use algebraic intuitions for introducing these nets and their reduction rules, and then we develop two correctness criteria (weak typeability and acyclicity) and show that they guarantee strong normalization. Finally, we outline the correspondence between this interaction nets formalism and the resource lambda-calculus. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect