Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755

Torben Ægidius Mogensen

doi:10.1007/3-540-46562-6_11

Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Abstract

We show that linear time self-interpretation of the pure untyped lambda calculus is possible. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.

We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term.

By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation and cost of an environment-based implementation.

For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.

Originalsprog	Engelsk
Titel	Perspectives of System Informatics : Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999 Proceedings
Forlag	Springer
Publikationsdato	2000
Sider	128-142
DOI	https://doi.org/10.1007/3-540-46562-6_11
Status	Udgivet - 2000
Begivenhed	3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics - Akademgorodok, Novosibirsk, Rusland Varighed: 6 jul. 1999 → 9 jul. 1999

Konference

Konference	3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics
Land/Område	Rusland
By	Akademgorodok, Novosibirsk
Periode	06/07/1999 → 09/07/1999

Navn	Lecture Notes in Computer Science
Vol/bind	1755 LNCS
ISSN	0302-9743

Adgang til dokumentet

10.1007/3-540-46562-6_11

Biblioteksadgang?

Tjek tilgængelighed hos det Kgl. Bibliotek

Citationsformater

Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755. / Mogensen, Torben Ægidius.
Perspectives of System Informatics: Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999 Proceedings. Springer, 2000. s. 128-142 (Lecture Notes in Computer Science, Bind 1755 LNCS).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Mogensen, TÆ 2000, Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755. i Perspectives of System Informatics: Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999 Proceedings. Springer, Lecture Notes in Computer Science, bind 1755 LNCS, s. 128-142, 3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics, Akademgorodok, Novosibirsk, Rusland, 06/07/1999. https://doi.org/10.1007/3-540-46562-6_11

Mogensen TÆ. Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755. I Perspectives of System Informatics: Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999 Proceedings. Springer. 2000. s. 128-142. (Lecture Notes in Computer Science, Bind 1755 LNCS). doi: 10.1007/3-540-46562-6_11

Mogensen, Torben Ægidius. / Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755. Perspectives of System Informatics: Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999 Proceedings. Springer, 2000. s. 128-142 (Lecture Notes in Computer Science, Bind 1755 LNCS).

@inproceedings{ac106da0e65511deba73000ea68e967b,

title = "Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755",

abstract = "We show that linear time self-interpretation of the pure untyped lambda calculus is possible. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term.By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.",

author = "Mogensen, {Torben {\AE}gidius}",

year = "2000",

doi = "10.1007/3-540-46562-6_11",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "128--142",

booktitle = "Perspectives of System Informatics",

address = "Switzerland",

note = "3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics ; Conference date: 06-07-1999 Through 09-07-1999",

}

TY - GEN

T1 - Linear-time self-interpretation of the pure lambda calculus, Lecture Notes in Computer Science, Vol.1755

AU - Mogensen, Torben Ægidius

PY - 2000

Y1 - 2000

N2 - We show that linear time self-interpretation of the pure untyped lambda calculus is possible. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term.By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.

AB - We show that linear time self-interpretation of the pure untyped lambda calculus is possible. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term.By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.

U2 - 10.1007/3-540-46562-6_11

DO - 10.1007/3-540-46562-6_11

M3 - Article in proceedings

T3 - Lecture Notes in Computer Science

SP - 128

EP - 142

BT - Perspectives of System Informatics

PB - Springer

T2 - 3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics

Y2 - 6 July 1999 through 9 July 1999

ER -