Adding Negation to Lambda Mu
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916122599620608 |
|---|---|
| author | van Bakel, Steffen |
| author_facet | van Bakel, Steffen |
| contents | We present $\cal L$, an extension of Parigot's $λμ$-calculus by adding negation as a type constructor, together with syntactic constructs that represent negation introduction and elimination. We will define a notion of reduction that extends $λμ$'s reduction system with two new reduction rules, and show that the system satisfies subject reduction. Using Aczel's generalisation of Tait and Martin-Löf's notion of parallel reduction, we show that this extended reduction is confluent. Although the notion of type assignment has its limitations with respect to representation of proofs in natural deduction with implication and negation, we will show that all propositions that can be shown in there have a witness in $\cal L$. Using Girard's approach of reducibility candidates, we show that all typeable terms are strongly normalisable, and conclude the paper by showing that type assignment for $\cal L$ enjoys the principal typing property. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2109_10447 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Adding Negation to Lambda Mu van Bakel, Steffen Logic in Computer Science We present $\cal L$, an extension of Parigot's $λμ$-calculus by adding negation as a type constructor, together with syntactic constructs that represent negation introduction and elimination. We will define a notion of reduction that extends $λμ$'s reduction system with two new reduction rules, and show that the system satisfies subject reduction. Using Aczel's generalisation of Tait and Martin-Löf's notion of parallel reduction, we show that this extended reduction is confluent. Although the notion of type assignment has its limitations with respect to representation of proofs in natural deduction with implication and negation, we will show that all propositions that can be shown in there have a witness in $\cal L$. Using Girard's approach of reducibility candidates, we show that all typeable terms are strongly normalisable, and conclude the paper by showing that type assignment for $\cal L$ enjoys the principal typing property. |
| title | Adding Negation to Lambda Mu |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2109.10447 |