Call-by-name, call-by-value and the λ-calculus. Plotkin, G. Theoretical Computer Science, 1(2):125–159, 1975. ISBN: 03043975doi abstract bibtex This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.
@article{plotkin_call-by-name_1975,
title = {Call-by-name, call-by-value and the λ-calculus},
volume = {1},
issn = {03043975},
doi = {10/d24k9b},
abstract = {This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.},
number = {2},
journal = {Theoretical Computer Science},
author = {Plotkin, G.D.},
year = {1975},
note = {ISBN: 03043975},
pages = {125--159}
}
Downloads: 0
{"_id":"SiEngXPFkku6DzpBo","bibbaseid":"plotkin-callbynamecallbyvalueandthecalculus-1975","authorIDs":[],"author_short":["Plotkin, G."],"bibdata":{"bibtype":"article","type":"article","title":"Call-by-name, call-by-value and the λ-calculus","volume":"1","issn":"03043975","doi":"10/d24k9b","abstract":"This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.","number":"2","journal":"Theoretical Computer Science","author":[{"propositions":[],"lastnames":["Plotkin"],"firstnames":["G.D."],"suffixes":[]}],"year":"1975","note":"ISBN: 03043975","pages":"125–159","bibtex":"@article{plotkin_call-by-name_1975,\n\ttitle = {Call-by-name, call-by-value and the λ-calculus},\n\tvolume = {1},\n\tissn = {03043975},\n\tdoi = {10/d24k9b},\n\tabstract = {This paper examines the old question of the relationship between ISWIM and the λ-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new λ-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual λ-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations.},\n\tnumber = {2},\n\tjournal = {Theoretical Computer Science},\n\tauthor = {Plotkin, G.D.},\n\tyear = {1975},\n\tnote = {ISBN: 03043975},\n\tpages = {125--159}\n}\n\n","author_short":["Plotkin, G."],"key":"plotkin_call-by-name_1975","id":"plotkin_call-by-name_1975","bibbaseid":"plotkin-callbynamecallbyvalueandthecalculus-1975","role":"author","urls":{},"downloads":0},"bibtype":"article","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.636Z","downloads":0,"keywords":[],"search_terms":["call","name","call","value","calculus","plotkin"],"title":"Call-by-name, call-by-value and the λ-calculus","year":1975,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}