A valid rule of beta-conversion for the logic of partial functions

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F17%3A86098994" target="_blank" >RIV/61989100:27240/17:86098994 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.klemens.sav.sk/fiusav/organon/?q=en/valid-rule-v-conversion-logic-partial-functions" target="_blank" >http://www.klemens.sav.sk/fiusav/organon/?q=en/valid-rule-v-conversion-logic-partial-functions</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

A valid rule of beta-conversion for the logic of partial functions

Popis výsledku v původním jazyce

The goal of this paper is to examine the conditions of validity for the rule of β-conversion in TIL, which is a hyperintensional, typed lambda-calculus of partial functions. The rule of β-reduction is a fundamental computational rule of the lambda-calculi and functional programming languages. However, it is a well-known fact that the specification of this rule is ambiguous. There are two procedurally non-equivalent ways of executing the rule, namely β-conversion ‘by name’ and β-conversion ‘by value’. In the lambda-calculi conversion by name is usually applied, though it is known that such a conversion is not unconditionally valid when partial functions are involved. If a procedure that is typed to produce an argument value is improper by failing to produce one, conversion by name cannot be validly applied. On the other hand, conversion by value is valid even in the case of improperness. Moreover, we show that in a typed lambda-calculus the specification of lambda-closure is also not unambiguous. There is an interpretation of this specification under which beta-reduction by name is not valid even when the argument procedure does not fail to produce a value. As a result, we present a universally valid rule of beta-reduction by value.

Název v anglickém jazyce

A valid rule of beta-conversion for the logic of partial functions

Popis výsledku anglicky

The goal of this paper is to examine the conditions of validity for the rule of β-conversion in TIL, which is a hyperintensional, typed lambda-calculus of partial functions. The rule of β-reduction is a fundamental computational rule of the lambda-calculi and functional programming languages. However, it is a well-known fact that the specification of this rule is ambiguous. There are two procedurally non-equivalent ways of executing the rule, namely β-conversion ‘by name’ and β-conversion ‘by value’. In the lambda-calculi conversion by name is usually applied, though it is known that such a conversion is not unconditionally valid when partial functions are involved. If a procedure that is typed to produce an argument value is improper by failing to produce one, conversion by name cannot be validly applied. On the other hand, conversion by value is valid even in the case of improperness. Moreover, we show that in a typed lambda-calculus the specification of lambda-closure is also not unambiguous. There is an interpretation of this specification under which beta-reduction by name is not valid even when the argument procedure does not fail to produce a value. As a result, we present a universally valid rule of beta-reduction by value.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10102 - Applied mathematics

Projekt

<a href="/cs/project/GA15-13277S" target="_blank" >GA15-13277S: Hyperintensionální logika pro analýzu přirozeného jazyka</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Organon F

ISSN

1335-0668

e-ISSN

—

Svazek periodika

24

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

SK - Slovenská republika

Počet stran výsledku

27

Strana od-do

10-36

Kód UT WoS článku

000397837700002

EID výsledku v databázi Scopus

2-s2.0-85017103356