The kernel strategy and its use for the study of combinatory logic (Q1311399)

The combinators \(S\) and \(K\) provide a basis for the study of all the combinatory logic. Fragments of this logic are usually studied instead, normally by replacing \(S\) and/or \(K\) by other combinators. Another strategy (the ``kernel strategy'') is proposed in this paper. It is very useful in studying questions concerned with fixed-point properties in relation to normal forms and paradoxes (applied in the context of an automated reasoning program). For each fragment studied, a kernel strategy (sound and complete) is used in attempt to determine whether the strong or the weak fixed-point property holds. ``To use the strategy, one selects a fragment of combinatory logic, a subset whose basis is obtained by replacing \(S\) and/or \(K\) by some set of combinators. If the first stage of the two-stage kernel strategy succeeds, then the fragment under study is proved to satisfy the weak fixed-point property and, further, to satisfy the reducible weak fixed-point property. The second stage of the strategy focuses on any successes of the first stage, each of which is called a kernel, and attempts to use the kernel to construct a fixed- point combinator. If the second stage succeeds, then the fragment is proved to satisfy the strong fixed-point property''. \textit{W. McCune} and the author's paper: ``The absence and the presence of fixed-point combinators'' [Theor. Comput. Sci. 87, No. 1, 221-228 (1991; Zbl 0731.03012)] may be consulted. Open problems are pointed out and direct applications for combinatory logic are emphasized.