Advertisement

λ-Terms as total or partial functions on normal forms

  • Corrado Böhm
  • Mariangiola Dezani-Ciancaglini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 37)

Abstract

In this paper the set of λ -terras is split into 2ω+1 disjoint classes Ph (−ω≤h≤ω). This classification takes into account the meaning of a λ-term F as function on normal forms, and more precisely:
  1. 1

    iff when auccessively applied to any number of normal forms it gives a λ-term without normal form

     
  2. 2

    (0<h<ω) iff when successively applied to h-1 arbitrary normal forms it gives a λ-term without normal form, but there exist h normal forms X1,...,Xh such that FX1...Xh possesses normal form

     
  3. 3

    (0≤h>ω) iff when successively applied to h arbitrary normal forms it gives a λ-term which possesses normal form, but there exist h+1 normal forms X1,...,Xh+1 such that FX1...Xh+1 possesses no normal form

     
  4. 4

    iff when successively applied to any number of normal forms it gives a λ-term which possesses normal form.

     

This classification can be effectively determined only for λ-terms in normal form.

Keywords

Normal Form Terminal Node Reduction Algorithm Current Variable Tree Representation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Böhm,C., The CUCH as a Formal and Description Language, Formal Language Description Languages for Computer Programming, ed.T.B. Steel, North-Holland, Amsterdam, (1966), 179–197.Google Scholar
  2. [2]
    Böhm,C., M.Dezani-Ciancaglini, Combinatorial Problems Combinator Equations and Normal Forms, Automata Languages and Programming, ed. J. Loeckx, Lecture Notes in Computer Science, 14, Springer-Verlag, (1974), 185–199.Google Scholar
  3. [3]
    Church,A., J.Barkley Rosser, Some properties of λ-conversion, Trans.Amer. Math Soc., 39, (1936), 472–482.Google Scholar
  4. [4]
    Curry, H.B., J.R. Hindley, J.P. Seldin, Combinatory Logic, 2, North-Holland, Amsterdam, (1972).Google Scholar
  5. [5]
    Knuth, D.E., Examples of Formal Semantics, Symposium on Semantics of Algorithmic Languages, 188, ed. E. Engeler, Springer-Verlag, Berlin, (1970), 212–235.Google Scholar
  6. [6]
    Simone, C., Un modello di λ-calcolo fortemente equivalente agli schemi ricorsivi, Calcolo, 1, (1974), 111–125.Google Scholar
  7. [7]
    Wadsworth, C.P., Semantics and Pragmatics of λ-calculus, Ph.D. Thesis, Oxford, (1971).Google Scholar
  8. [8]
    Welch, P.H., Continuous Semantics and Inside-Outside Reductions, these Proceedings.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1975

Authors and Affiliations

  • Corrado Böhm
    • 1
  • Mariangiola Dezani-Ciancaglini
    • 2
  1. 1.Istituto Matematico G. CastelnuovoUniversità di RomaItaly
  2. 2.Istituto di Scienza dell' InformazioneUniversità di TorinoItaly

Personalised recommendations