Programs as Data Structures in λSF-Calculus

Jay, B

Programs as Data Structures in λSF-Calculus

Jay, B

Permalink

Publication Type:: Journal Article
Citation:: Electronic Notes in Theoretical Computer Science, 2016, 325 pp. 221 - 236
Issue Date:: 2016-10-05

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Published VersionAdobe PDF (238.41 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.date.issued	2016-10-05	en_US
dc.identifier.citation	Electronic Notes in Theoretical Computer Science, 2016, 325 pp. 221 - 236	en_US
dc.identifier.issn	1571-0661	en_US
dc.identifier.uri	http://hdl.handle.net/10453/122938
dc.description.abstract	© 2016 The Author(s) Lambda-SF-calculus can represent programs as closed normal forms. In turn, all closed normal forms are data structures, in the sense that their internal structure is accessible through queries defined in the calculus, even to the point of constructing the Goedel number of a program. Thus, program analysis and optimisation can be performed entirely within the calculus, without requiring any meta-level process of quotation to produce a data structure. Lambda-SF-calculus is a confluent, applicative rewriting system derived from lambda-calculus, and the combinatory SF-calculus. Its superior expressive power relative to lambda-calculus is demonstrated by the ability to decide if two programs are syntactically equal, or to determine if a program uses its input. Indeed, there is no homomorphism of applicative rewriting systems from lambda-SF-calculus to lambda-calculus. Program analysis and optimisation can be illustrated by considering the conversion of a programs to combinators. Traditionally, a program p is interpreted using fixpoint constructions that do not have normal forms, but combinatory techniques can be used to block reduction until the program arguments are given. That is, p is interpreted by a closed normal form M. Then factorisation (by F) adapts the traditional account of lambda-abstraction in combinatory logic to convert M to a combinator N that is equivalent to M in the following two senses. First, N is extensionally equivalent to M where extensional equivalence is defined in terms of eta-reduction. Second, the conversion is an intensional equivalence in that it does not lose any information, and so can be reversed by another definable conversion. Further, the standard optimisations of the conversion process are all definable within lambda-SF-calculus, even those involving free variable analysis. Proofs of all theorems in the paper have been verified using the Coq theorem prover.	en_US
dc.relation.ispartof	Electronic Notes in Theoretical Computer Science	en_US
dc.relation.isbasedon	10.1016/j.entcs.2016.09.040	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Programs as Data Structures in λSF-Calculus	en_US
dc.type	Journal Article
utslib.citation.volume	325	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0803 Computer Software	en_US
utslib.for	1702 Cognitive Sciences	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/Strength - CAI - Centre for Artificial Intelligence
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	325	en_US

Abstract:

© 2016 The Author(s) Lambda-SF-calculus can represent programs as closed normal forms. In turn, all closed normal forms are data structures, in the sense that their internal structure is accessible through queries defined in the calculus, even to the point of constructing the Goedel number of a program. Thus, program analysis and optimisation can be performed entirely within the calculus, without requiring any meta-level process of quotation to produce a data structure. Lambda-SF-calculus is a confluent, applicative rewriting system derived from lambda-calculus, and the combinatory SF-calculus. Its superior expressive power relative to lambda-calculus is demonstrated by the ability to decide if two programs are syntactically equal, or to determine if a program uses its input. Indeed, there is no homomorphism of applicative rewriting systems from lambda-SF-calculus to lambda-calculus. Program analysis and optimisation can be illustrated by considering the conversion of a programs to combinators. Traditionally, a program p is interpreted using fixpoint constructions that do not have normal forms, but combinatory techniques can be used to block reduction until the program arguments are given. That is, p is interpreted by a closed normal form M. Then factorisation (by F) adapts the traditional account of lambda-abstraction in combinatory logic to convert M to a combinator N that is equivalent to M in the following two senses. First, N is extensionally equivalent to M where extensional equivalence is defined in terms of eta-reduction. Second, the conversion is an intensional equivalence in that it does not lose any information, and so can be reversed by another definable conversion. Further, the standard optimisations of the conversion process are all definable within lambda-SF-calculus, even those involving free variable analysis. Proofs of all theorems in the paper have been verified using the Coq theorem prover.

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

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