Minimal forms in lambda-calculus computations. (English) Zbl 0451.03002
Der \(\lambda\)-Kalkül wird als Berechnungsmodell (computation model) betrachtet und die Relation \(A\triangleright B\) als transitive Hülle der Reduktion \(F\to G\) daraufhin untersucht, ob sie eine minimale Form hat. In §1 werden die Begriffe der Normal- und Minimalform eingeführt und der Beweis erbracht, daß die Menge der Terme, die Minimalformen haben, nicht eine rekursive Menge ist. Ferner wird unter Anwendung einer Strategie (cofinal strategy) gezeigt, wann ein Term eine Minimalform hat. In §2 wird dann die Knuth-Gross-Strategie (G) als cofinal strategy eingeführt und als Theorem 5 bewiesen, daß \(A\) genau dann in Minimalform ist, wenn die Strategie G auf \(A\) angewandt auf \(A\) führt, woraus ein Algorithmus zur Bestimmung der Minimalform folgt. Schließlich wird gezeigt, daß die Eigenschaft eines generischen Terms, eine Minimalform zu haben, ein semi-entscheidbares Prädikat ist.
Reviewer: R. Nabert
MSC:
03B40 | Combinatory logic and lambda calculus |
03D60 | Computability and recursion theory on ordinals, admissible sets, etc. |
03D25 | Recursively (computably) enumerable sets and degrees |
References:
[1] | Combinatory logic 1 (1958) |
[2] | Annals of Mathematical Studies (1941) |
[3] | Degrees, reductions and representability (1976) |
[4] | Lecture Notes in Computer Science 37 pp 367– (1975) |
[5] | Proceedings of the Sth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science pp 477– (1978) |
[6] | Standard and normal reductions (1975) |
[7] | Computahility and {\(\lambda\)}-definability 2 pp 153– (1937) |
[8] | Toposes, algebraic geometry and logic, Lecture Notes in Mathematics (1972) |
[9] | Journées des Mathématiques de la Compilations (1973) |
[10] | Symposium on semantics of algorithmic languages, Lecture Notes in Mathematics 188 pp 212– (1970) |
[11] | The p-function in {\(\lambda\)}-K-conversion 2 pp 164– (1937) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.