Treffer: Termination analysis of the untyped λ-calculus

Title:
Termination analysis of the untyped λ-calculus
Authors:
JONES, Neil D, BOHR, Nina
Source:
RTA 2004 : rewriting techniques and applications (Aachen, 3-5 June 2004)Lecture notes in computer science. :1-23
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 9 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Algorithme récursif, Recursive algorithm, Algoritmo recursivo, Fonction récursive, Recursive function, Función recursiva, Lambda calcul, Lambda calculus, Lambda cálculo, Problème terminaison, Termination problem, Problema terminación, Programme récursif, Recursive program, Programa recursivo, Analyse terminaison, Termination analysis, Análisis terminación, Appel par valeur, Call by value, Llamada por valor
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
DIKU, University of Copenhagen, Denmark
IT University of Copenhagen, Denmark
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=15851900
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15851900
Database:
PASCAL Archive

Weitere Informationen

An algorithm is developed that, given an untyped λ-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the size-change principle earlier applied to first-order programs. The algorithm is sound (and proven so in this paper) but not complete: some A-expressions may in fact terminate under call-by-value evaluation, but not be recognised as terminating. The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's minimum algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF. The extensional power of size-change termination is the set of functions computable by size-change terminating programs. This lies somewhere between Péter's multiple recursive functions and the class of ∈0-recursive functions.