A Combinatory Account of Internal Structure

Publisher:
Assn Symbolic Logic Inc
Publication Type:
Journal Article
Citation:
Journal Of Symbolic Logic, 2011, 76 (3), pp. 807 - 826
Issue Date:
2011-01
Full metadata record
Files in This Item:
Filename Description Size
Thumbnail2010003973.pdf200.59 kB
Adobe PDF
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.
Please use this identifier to cite or link to this item: