Abstract
This paper describes a machine for reducing a λ-formula (explicitly given or implicitly by a system of recursive equations) to principal β-η-normal form, with particular attention to the memory structures needed for the purpose, and with some important features: (1) any kind of collision is permitted; (2) the processing of subformulas which will be thrown away [e.g., ((λxy)x) in ((λyz)(λxy)x)] is avoided; (3) there is no need to introduce any fixed point operator like ϕ, etc. The machine structure entails: (1) some store to memorize as side-effects assignment statements with the r.h.s. of a given shape. (2) a number of stacks, one for every λ in the initial formula, partitioned naturally in classes (chains). These stacks admit as entries only words representing variables and they are peculiar in that the operations admitted on the top arewriting anderasing and the operations admitted on the pseudo-top arereading,read-protecting, andresetting readability (the last two operations are chain operations). This structure is critically motivated. (3) A workstack. (4) A pointerstack. The computation runs through four phases: β-generation, β-run, η-generation, η-run. Every generation- (run-) phase is rather recognition- (transformation-) oriented, but we found it more stimulating to emphasize technical similarities rather than methodological differences. Every phase is described and four examples are extensively developed.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
G. Ausiello, “Automatic reduction of CUCH expressions by means of the value method,”Atti del I Congresso Nazionale dell'AICA, Napoli 26–29 settembre 1968 (Rome, 1971), pp. 174–184.
C. Böhm and W. Gross, “Introduction to the CUCH,” inAutomata Theory, ed. by E. R. Caianiello (Academic Press, New York, 1966), pp. 35–65.
C. Böhm, “The CUCH as a formal and description language,” inFormal Languages Description Languages for Computer Programming,” ed. by T. B. Steel, Jr. (North-Holland, Amsterdam, 1966), pp. 179–197.
A. Church, “The calculi of lambda-conversion,” Ann. Math. Stud. No. 6, Princeton University Press, 1941.
J. B. Curry and R. Feys,Combinatory Logic, Vol. 1 (North-Holland, Amsterdam, 1958).
S. Ginsburg, Sheila A. Greibach, and Michael A. Harrison, “One-way stack automata,”ACM,14(2): 389–418 (1967).
P. Landin, “A correspondence between ALGOL 60 and Church's lambda notation,”Comm. ACM (February/March 1965).
D. Scott, “Outline of a mathematical theory of computation,” Oxford University Computing Laboratory Programming Research Group (1970).
C. Strachey, “Towards a formal semantics,” inFormal Languages Description Languages, for Computer Programming, ed. by T. B. Steel, Jr. (North-Holland, Amsterdam, 1966), pp. 198–216.
P. Wegner,Programming Languages, Information Structures and Machine Organisation (McGraw-Hill, New York, 1968).
C. McGowan, “The correctness of a modified SECD machine,” 2nd Annual ACM Symposium on the Theory of Computation, 1970, North Hampton, pp. 149–157.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Böhm, C., Dezani, M. A CUCH-machine: The automatic treatment of bound variables. International Journal of Computer and Information Sciences 1, 171–191 (1972). https://doi.org/10.1007/BF00995737
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00995737