Termination tests inside λ-calculus

  • C. Böhm
  • M. Coppo
  • M. Dezani-Ciancaglini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 52)


Let be associated to each element N of the set
of the normal forms of the λ-κ-β calculus and to each integer r > 0 the semi but non - decidable domain D [N,r] \( \subseteq \)
r onto which N, considered as partial map ping
, is total (that is the computation starting from NX1 ... Xr where N ∈
and X1, ..., xrD [N,r] and evolging through a β -reduction algorithm terminates). The decidability of the relation D [N,r] =
r has been proved in a previous paper. In the present paper, for any N and r, an infinite, decidable subdomain C [N,r] \( \subseteq \)D [N,r] is defined in a constructive way. The ensuing sufficient condition for the termination of a computation starting from N X1 ... Xr can be tested in a number of steps negligible with respect to those needed for reaching the n.f., if there is one.


Normal Form Composition Operator Free Variable Combinatory Logic Access Path 
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.


  1. [1]
    C. BÖHM, 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]
    C. BÖHM, Alcune proprietà delle forme β-η-normali nel λ-κ-calcolo, IAC, (1968), 696.Google Scholar
  3. [3]
    C. BÖHM, M. DEZANI-CIANCAGLINI, λ-term as Total or Partial Functions on Normal Forms, λ-Calculus and Computer Science Theory, ed. C. Böhm, Lecture Notes in Computer Science, 37, Springer-Verlag, (1975), 96–121.Google Scholar
  4. [4]
    H.B. CURRY, R. FEYS, Combinatory Logic, 1, North-Holland, Amsterdam, (1958).Google Scholar
  5. [5]
    H.B. CURRY, R. HINDLEY, J.P. SELDIN, Combinatory Logic, 2, North-Holland, Amsterdam, (1972).Google Scholar
  6. [6]
    M. DEZANI-CIANCAGLINI, A Type Theory for λ-β-normal Forms, Proc. of the Symposium Informatica 75, Bled, (1975).Google Scholar
  7. [7]
    M. DEZANI-CIANCAGLINI, S. RONCHI DELLA ROCCA, Computational Complexity and Structure of λ-terms, Programming, ed. B. Robinet, Dunod, Paris, (1976), 160–181.Google Scholar
  8. [8]
    S. STENLUND, Combinators, λ-terms and Proof Theory, D. Reidel Publ. Company, Dordrecht-Holland, (1972).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1977

Authors and Affiliations

  • C. Böhm
    • 1
  • M. Coppo
    • 2
  • M. Dezani-Ciancaglini
    • 3
  1. 1.Istituto Matematico G. Castelnuovo (Università di Roma)Italy
  2. 2.Istituto di Scienza dell'Informazione (Università di Torino)Italy
  3. 3.Istituto di Scienza dell'Informazione (Università di Torino)Italy

Personalised recommendations