An extended type system with lambda-typed lambda-expressions
We present the system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential abstraction operator as well as propositional operators. $\beta$...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4409/pdf |
| _version_ | 1797268560993583104 |
|---|---|
| author | Matthias Weber |
| author_facet | Matthias Weber |
| author_sort | Matthias Weber |
| collection | DOAJ |
| description | We present the system $\mathtt{d}$, an extended type system with lambda-typed
lambda-expressions. It is related to type systems originating from the Automath
project. $\mathtt{d}$ extends existing lambda-typed systems by an existential
abstraction operator as well as propositional operators. $\beta$-reduction is
extended to also normalize negated expressions using a subset of the laws of
classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas
which are handled uniformly as functional expressions. $\mathtt{d}$ is using a
reflexive type axiom for a constant $\tau$ to which no function can be typed.
Some properties are shown including confluence, subject reduction, uniqueness
of types, strong normalization, and consistency. We illustrate how, when using
$\mathtt{d}$, due to its limited logical strength, additional axioms must be
added both for negation and for the mathematical structures whose deductions
are to be formalized. |
| first_indexed | 2024-04-25T01:34:26Z |
| format | Article |
| id | doaj.art-5bf114c91ef24461a530a7d1b302e683 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:26Z |
| publishDate | 2020-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5bf114c91ef24461a530a7d1b302e6832024-03-08T10:32:05ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-12-01Volume 16, Issue 410.23638/LMCS-16(4:12)20204409An extended type system with lambda-typed lambda-expressionsMatthias WeberWe present the system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt{d}$ extends existing lambda-typed systems by an existential abstraction operator as well as propositional operators. $\beta$-reduction is extended to also normalize negated expressions using a subset of the laws of classical negation, hence $\mathtt{d}$ is normalizing both proofs and formulas which are handled uniformly as functional expressions. $\mathtt{d}$ is using a reflexive type axiom for a constant $\tau$ to which no function can be typed. Some properties are shown including confluence, subject reduction, uniqueness of types, strong normalization, and consistency. We illustrate how, when using $\mathtt{d}$, due to its limited logical strength, additional axioms must be added both for negation and for the mathematical structures whose deductions are to be formalized.https://lmcs.episciences.org/4409/pdfcomputer science - logic in computer science |
| spellingShingle | Matthias Weber An extended type system with lambda-typed lambda-expressions Logical Methods in Computer Science computer science - logic in computer science |
| title | An extended type system with lambda-typed lambda-expressions |
| title_full | An extended type system with lambda-typed lambda-expressions |
| title_fullStr | An extended type system with lambda-typed lambda-expressions |
| title_full_unstemmed | An extended type system with lambda-typed lambda-expressions |
| title_short | An extended type system with lambda-typed lambda-expressions |
| title_sort | extended type system with lambda typed lambda expressions |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/4409/pdf |
| work_keys_str_mv | AT matthiasweber anextendedtypesystemwithlambdatypedlambdaexpressions AT matthiasweber extendedtypesystemwithlambdatypedlambdaexpressions |