Detail príspevku/publikácie

A Valid Rule of β-conversion for the Logic of Partial Functions

Kosterec, Miloš
Duží, Marie
Organon F, 2017, vol. 24, No 1, pp. 10-36.
Súbor na stiahnutie: PDF
BibTex EndNote Tagged EndNote XML RIS
The goal of this paper is to examine the conditions of validity for the rule of β-conversion in TIL, which is a hyperintensional, typed λ-calculus of partial functions. The rule of β-reduction is a fundamental computational rule of the λ-calculi and functional programming languages. However, it is a well-known fact that the specification of this rule is ambiguous (see, e.g., Plotkin 1975 or Chang & Felleisen 2012). There are two procedurally non-equivalent ways of executing the rule, namely β-conversion ‘by name’ and β-conversion ‘by value’. In the λ-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 λ-calculus the specification of λ-closure is also not unambiguous. There is an interpretation of this specification under which β-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 β-reduction by value.

Kontakt

Filozofický ústav SAV, v. v. i.
Klemensova 19
811 09 Bratislava 1
Tel.: +4212 5292 1215
E-mail: sekretariat.fiu@savba.sk
Domovská stránka
IČO: 00166995
DIČ: 2020794149

Korešpondenčná adresa:

Filozofický ústav SAV, v. v. i.
P. O. Box 3364
813 64 Bratislava

Filozofia - redakcia

Filozofický ústav SAV, v. v. i.
Redakcia časopisu Filozofia
Klemensova 19
811 09 Bratislava 1
Tel.: +4212 5292 1215
E-mail: redakcia.filozofia@savba.sk
Domovská stránka

Korešpondenčná adresa:

Filozofický ústav SAV, v. v. i.
Redakcia časopisu Filozofia
P. O. Box 3364
813 64 Bratislava

Organon F - redakcia

Filozofický ústav SAV, v. v. i.
Redakcia časopisu Organon F
Klemensova 19
811 09 Bratislava 1
Tel.: +4212 5292 1215
E-mail: info@organonf.com
Domovská stránka

Korešpondenčná adresa:

Filozofický ústav SAV, v. v. i.
Redakcia časopisu Organon F
P. O. Box 3364
813 64 Bratislava