Derivability of rules of beta-conversion in partial type theory

RACLAVSKÝ, Jiří and Petr KUCHYŇKA. Derivability of rules of beta-conversion in partial type theory. In Czech Gathering of Logicians (CGL2022). 2022.

Basic information

• Original name: Derivability of 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: Czech Gathering of Logicians (CGL2022), 2022.

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: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14210/22:00129978
• Organization unit: Faculty of Arts
• Keywords in English: beta-reduction; partial type theory; partial lambda-calculus; natural deduction
• Tags: Reviewed

Abstract

In partial type theory (PTT), the rules of beta-conversion should be appropriately conditioned in order to preserve their validity which can be negatively affected by partiality (non-denoting expressions). After showing that within a particular natural deduction for PTT, we derive also their novel variants which allow inferences not permissible using the original variants. Moreover, we derive even versions that substitute value (resembling call-by-value evaluation).

Links

• MUNI/A/1088/2021, interní kód MU: Name: Aspekty soudobé filozofie IV

Investor: Masaryk University