Call-by-name, call-by-value and the λ-calculus Export

@article{citeulike:467090, 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.}, author = {Plotkin, G.}, citeulike-article-id = {467090}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/0304-3975(75)90017-1}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/0304-3975(75)90017-1}, citeulike-linkout-2 = {http://www.sciencedirect.com/science/article/B6V1G-46922HH-3/2/a20b91fda9c99ea8a205f1b1d03237ae}, doi = {10.1016/0304-3975(75)90017-1}, issn = {03043975}, journal = {Theoretical Computer Science}, keywords = {lambda-calculus}, month = {December}, number = {2}, pages = {125--159}, posted-at = {2008-02-14 13:22:15}, priority = {2}, title = {Call-by-name, call-by-value and the λ-calculus}, url = {http://dx.doi.org/10.1016/0304-3975(75)90017-1}, volume = {1}, year = {1975} }

TY - JOUR ID - citeulike:467090 L3 - citeulike-article-id:467090 N2 - 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. IS - 2 JF - Theoretical Computer Science SN - 03043975 EP - 159 TI - Call-by-name, call-by-value and the λ-calculus VL - 1 SP - 125 KW - lambda-calculus AU - Plotkin, G PY - 1975/12// UR - http://dx.doi.org/10.1016/0304-3975(75)90017-1 ER -