NDLI: Comments on Georgeff's “transformations and reduction strategies for typed lambda expressions”

Content Provider	ACM Digital Library
Author	Nielson, Hanne Rus Nielson, Flemming
Copyright Year	1986
Abstract	In his recent paper, Georgeff [1] considers the evaluation of lambda expres sions (with reducing reflexive types) on a variant of Landin's SECD machine. It is observed that for so-called simple expressions the SECD machine will construct stack-like environment structures, whereas, in general, they are tree-like. Georgeff then explores the idea of transforming any (typed) lambda expression into simple form and then using the SECD machine for these expressions. However, such transformations might be undesirable if the language is going to be interpreted directly. This leads Georgeff to modify the SECD machine such that it constructs stack-like environments for all expressions.Briefly, the idea in this modification is to let the machine construct over-applied closures for function-valued expressions in operand positions and to let it apply the closure in situ in the case of function-valued expressions in operator positions. The construction of overapplied closures implies that tree- like environment structures are avoided. Georgeff claims that by applying expressions in operator positions in situ it is avoided that operand values are “needlessly popped from the stack during creation of the overapplied closure, only to be reinstated on entry to the closure” [ 1, p. 620]. However, the example of Figure 1 shows that Georgeff's construction does not overcome this problem: the transitions 14, 15, and 16 move the on constant 3 from the stack to the closure and back to the stack. Intuitively, the reason is that the construction does not recognize correctly whether a sub-expression in operator position is in fact “basic-valued.” An expression (or, more precisely, its closure) occurring in operator position will look for its remaining arguments on the current stack and on the stacks of the dump. The prediction of the number of available arguments is important in order to determine whether the expression is “basic-valued,” and should therefore be treated specially.Georgeff suggests the following function for counting the number of avail-able arguments on the stacks:def totapps (ST)let (S, E, C, D) = STlet $\textit{n}$ = (napps C)if $\textit{n}$ = 0 then $\textit{n}else$ (+ n (totapps D))endwhere the function (napps C) returns the number of consecutive apply operators at the beginning of the control C. For the configuration of line 14 of Figure 1 this gives totapps (. . .) = 2 napps (A&aacgr;A) = 1 and totapps (d1) = 1 — this means that the closure [(βγ), u, (2), e1] can find 2 arguments on the stacks although its functionality is 1! Hence, the predicate, basic-valued, fails, although it ought to succeed.We suggest replacing the function above with def totapps (ST)let (S, E, C, D) = STlet $\textit{n}$ = (napps C)if length C ≠ $\textit{n}$ then,/B> $\textit{n}else$ (+ $\textit{n}$ (totapps D))endwhere length C is the length of the list C. The intuition behind this suggestion is that, if the control C of some configuration is not just a list of apply symbols, then the subexpression at hand will be turned into operand position before a basic value can be returned. Returning to the example mentioned above, note that we now get totapps (...) = 1 because napps (A&aacgr;A) = 1 and length (A&aacgr;A) ≠ 1, and the needless movements on the stack are avoided.
Starting Page	406
Ending Page	407
Page Count	2
File Format	PDF
ISSN	01640925
e-ISSN	15584593
DOI	10.1145/5956.215007
Volume Number	8
Issue Number	3
Journal	ACM Transactions on Programming Languages and Systems (TOPLAS)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1986-06-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Transformations and reduction strategies for typed lambda expressions

Strongly typed flow-directed representation transformations (extended abstract)

Compact bit encoding schemes for simply-typed lambda-terms

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

Preprocessing of typed two-dimensional mathematical expressions

Handling Operator Precedence in Arithmetic Expressions with Tree Transformations

The Lambda Lambda-Bar calculus:a dual calculus for unconstrained strategies

Typed self-representation

Static typing for a faulty lambda calculus

Comments on Georgeff's “transformations and reduction strategies for typed lambda expressions”

Similar Documents

Transformations and reduction strategies for typed lambda expressions

Strongly typed flow-directed representation transformations (extended abstract)

Compact bit encoding schemes for simply-typed lambda-terms

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

Preprocessing of typed two-dimensional mathematical expressions

Handling Operator Precedence in Arithmetic Expressions with Tree Transformations

The Lambda Lambda-Bar calculus:a dual calculus for unconstrained strategies

Typed self-representation

Static typing for a faulty lambda calculus

Comments on Georgeff's “transformations and reduction strategies for typed lambda expressions”