A combinatory account of internal structure

Jay, B; Given-Wilson, T

A combinatory account of internal structure

Jay, B

Given-Wilson, T

Permalink

Publication Type:: Journal Article
Citation:: Journal of Symbolic Logic, 2011, 76 (3), pp. 807 - 826
Issue Date:: 2011-09-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download full textAdobe PDF (200.59 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Jay, B https://orcid.org/0000-0001-8654-4305	en_US
dc.contributor.author	Given-Wilson, T https://orcid.org/0000-0001-8700-2671	en_US
dc.date.issued	2011-09-01	en_US
dc.identifier.citation	Journal of Symbolic Logic, 2011, 76 (3), pp. 807 - 826	en_US
dc.identifier.issn	0022-4812	en_US
dc.identifier.uri	http://hdl.handle.net/10453/14486
dc.description.abstract	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. © 2011, Association for Symbolic Logic.	en_US
dc.relation.ispartof	Journal of Symbolic Logic	en_US
dc.relation.isbasedon	10.2178/jsl/1309952521	en_US
dc.subject.classification	General Mathematics	en_US
dc.title	A combinatory account of internal structure	en_US
dc.type	Journal Article
utslib.citation.volume	3	en_US
utslib.citation.volume	76	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0101 Pure Mathematics	en_US
utslib.for	2203 Philosophy	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Computer Science
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Software
pubs.organisational-group	/University of Technology Sydney/Strength - CAI - Centre for Artificial Intelligence
utslib.copyright.status	open_access
pubs.issue	3	en_US
pubs.publication-status	Published	en_US
pubs.volume	76	en_US

Abstract:

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. © 2011, Association for Symbolic Logic.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/14486