| Autor: |
Vaux, Lionel |
| Přispěvatelé: |
Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Aix-Marseille Université, Paul-André Melliès |
| Jazyk: |
francouzština |
| Rok vydání: |
2021 |
| Předmět: |
|
| Zdroj: |
Logique en informatique [cs.LO]. Aix-Marseille Université, 2021 |
| Popis: |
Le développement de Taylor des λ-termes et des preuves de la logique linéaire est le fruit d’une relecture syntaxique par Ehrhard et Regnier de la sémantique quantitative de Girard : il associe à chaque terme ou preuve une combinaison linéaire infinie d’approximations multilinéaires et finies de l’objet de départ. Il matérialise une correspondance étroite entre le comportement calculatoire des termes, défini par la β-réduction, et leur interprétation dans certains modèles dénotationnels : le développement de Taylor d’un terme est toujours normalisable, et sa forme normale correspond exactement à l’arbre de Böhm du terme. Cette correspondance se retrouve dans le fait que, pour de nombreux modèles de la logique linéaire, la promotion d’un morphisme s’obtient comme une superposition d’opérations multilinéaires, faisant du développement de Taylor des preuves une structure sous-jacente de ces modèles.Ce mémoire présente quelques avancées récentes visant à raffiner l’analyse de la normalisation (qui est un processus potentiellement infini) offerte par le développement de Taylor pour la ramener au niveau de la β-réduction ou de l’élimination des coupures (qui correspond à un calcul fini).On démontre que cette approche permet d’étendre l’analyse à un cadre non-uniforme, susceptible de prendre en compte par exemple une forme de non-déterminisme calculatoire — alors que la normalisation peut échouer dans ce cadre. On démontre également que la même approche peut être appliquée aux réseaux de démonstration de la logique linéaire. Enfin les techniques développées précédemment permettent de revisiter et simplifier le résultat originel d’Ehrhard et Regnier pour la normalisation dans le cas uniforme, tout en l’adaptant à une forme restreinte de non-déterminisme. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
