Novel rules of beta-conversion in partial type theory

RACLAVSKÝ, Jiří and Petr KUCHYŇKA. Novel rules of beta-conversion in partial type theory. In 27th International Conference on Types for Proofs and Programs (TYPES2021), Nizozemí (online), 14. - 18. 6. 2021. 2021.

Basic information

• Original name: Novel rules of beta-conversion in partial type theory
• Authors: RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution) and Petr KUCHYŇKA (203 Czech Republic).
• Edition: 27th International Conference on Types for Proofs and Programs (TYPES2021), Nizozemí (online), 14. - 18. 6. 2021, 2021.

Other information

• Original language: English
• Type of outcome: Presentations at conferences
• Field of Study: 60301 Philosophy, History and Philosophy of science and technology
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14210/21:00119013
• Organization unit: Faculty of Arts
• Keywords in English: beta-reduction; partial type theory; partial lambda-calculus; explicit substitution; partiality; natural deduction
• Tags: rivok
• Tags: International impact, Reviewed

Abstract

In partial type theory, i.e. a higher-order logical system that manipulates both total and partial functions, a precise formulation of valid rules of $\beta$-conversion and even their versions that substitute a value is possible if explicit substitution and two special evaluation terms are involved. We derive the latter rules from the primary versions of $\beta$-conversion rules and other primitive rules of the natural deduction for the system. In addition, we formulate and derive further novel variants of $\beta$-conversion rules which are also needed for capturing inferences with terms that denote partial functions.

Links

• GA19-12420S, research and development project: Name: Hyperintenzionální význam, teorie typů a logická dedukce (Acronym: Hyperintensionality and Types)

Investor: Czech Science Foundation