A CUCH-machine: The automatic treatment of bound variables

  • Corrado Böhm
  • Mariangiola Dezani
Article

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    A. Church, “The calculi of lambda-conversion,” Ann. Math. Stud. No. 6, Princeton University Press, 1941.Google Scholar
  5. 5.
    J. B. Curry and R. Feys,Combinatory Logic, Vol. 1 (North-Holland, Amsterdam, 1958).Google Scholar
  6. 6.
    S. Ginsburg, Sheila A. Greibach, and Michael A. Harrison, “One-way stack automata,”ACM,14(2): 389–418 (1967).Google Scholar
  7. 7.
    P. Landin, “A correspondence between ALGOL 60 and Church's lambda notation,”Comm. ACM (February/March 1965).Google Scholar
  8. 8.
    D. Scott, “Outline of a mathematical theory of computation,” Oxford University Computing Laboratory Programming Research Group (1970).Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    P. Wegner,Programming Languages, Information Structures and Machine Organisation (McGraw-Hill, New York, 1968).Google Scholar
  11. 11.
    C. McGowan, “The correctness of a modified SECD machine,” 2nd Annual ACM Symposium on the Theory of Computation, 1970, North Hampton, pp. 149–157.Google Scholar

Copyright information

© Plenum Publishing Corporation 1972

Authors and Affiliations

  • Corrado Böhm
    • 1
  • Mariangiola Dezani
    • 1
  1. 1.Istituto di Scienza della InformazioneUniversitá di TorinoItaly

Personalised recommendations