Matthias Weber - An extended type system with lambda-typed lambda-expressions

lmcs:4409 - Logical Methods in Computer Science, December 1, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:12)2020
An extended type system with lambda-typed lambda-expressionsArticle

Authors: Matthias Weber

    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.


    Volume: Volume 16, Issue 4
    Published on: December 1, 2020
    Accepted on: August 19, 2020
    Submitted on: March 28, 2018
    Keywords: Computer Science - Logic in Computer Science

    References

    Consultation statistics

    This page has been seen 709 times.
    This article's PDF has been downloaded 172 times.