A combinatory account of internal structure. (English) Zbl 1248.03025

Summary: Traditional combinatory logic uses combinators S and K to represent all Turing-computable functions on natural numbers, but there are Turing-computable functions on the combinators themselves that cannot be so represented, because they access internal structure in ways that S and K cannot. Much of this expressive power is captured by adding a factorisation combinator F. The resulting SF-calculus is structure-complete, in that it supports all pattern-matching functions whose patterns are in normal form, including a function that decides structural equality of arbitrary normal forms. A general characterisation of the structure-complete, confluent combinatory calculi is given along with some examples. These are able to represent all their Turing-computable functions whose domain is limited to normal forms. The combinator F can be typed using an existential type to represent internal type information.


03B40 Combinatory logic and lambda calculus
03B70 Logic in computer science
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
Full Text: DOI


[1] DOI: 10.1007/BF01448013 · JFM 50.0023.01
[2] Logic, semantics, metamathematics (1956)
[3] DOI: 10.1145/367177.367199 · Zbl 0101.10413
[4] Handbook of theoretical computer science B (1990)
[5] Proofs and types (1989) · Zbl 0671.68002
[6] 2nd Scandinavian logic symposium (1971)
[7] Combinatory logic II (1972) · Zbl 0242.02029
[8] Combinatory logic I (1958)
[9] DOI: 10.2307/2371045 · Zbl 0014.09802
[10] DOI: 10.1093/comjnl/12.1.41 · Zbl 0164.46202
[11] The lambda calculus. Its syntax and semantics (1985)
[12] Introduction to higher-order categorical logic 7 (1986) · Zbl 0596.03002
[13] Introduction to metamathematics (1952)
[14] DOI: 10.1305/ndjfl/1093890995
[15] Combinatory logic with discriminators 34 pp 561– (1969)
[16] DOI: 10.1145/1034774.1034775 · Zbl 05459224
[17] DOI: 10.1017/S0956796808007144 · Zbl 1163.68315
[18] Programming languages and systems, 15th European Symposium on Programming, ESOP 2006 3924 pp 100– (2006)
[19] Pattern calculus: Computing with Junctions and data structures (2009)
[20] DOI: 10.1145/322217.322230 · Zbl 0458.68007
[21] Introduction to combinators and {\(\lambda\)}-calculus (1986) · Zbl 0614.03014
[22] Transactions of the American Mathematical Society 144 pp 1– (1969)
[23] Computability and {\(\lambda\)}-definability 2 pp 153– (1937)
[24] DOI: 10.1145/321738.321750 · Zbl 0267.68013
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.