Skip to main content

Encoding the Factorisation Calculus

Rowe, Reuben (2015) Encoding the Factorisation Calculus. In: Electronic Proceedings in Theoretical Computer Science. Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics. 190. pp. 76-90. (doi:10.4204/EPTCS.190.6) (KAR id:64718)

PDF Author's Accepted Manuscript
Language: English

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (240kB) Preview
Official URL


Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural completeness, i.e. it is able to represent any function on terms definable using pattern matching on arbitrary normal forms. In particular, it admits a term that can decide the structural equality of any two arbitrary normal forms.

This paper begins to bridge that gap by presenting a faithful encoding of the Factorisation Calculus into the Lambda Calculus preserving both reduction and strong normalisation. The existence of such an encoding is a new result. It also suggests that there is, in some sense, an equivalence between the former model and the latter. We discuss to what extent our result constitutes an equivalence by considering it in the context of some previously defined frameworks for comparing computational power and expressiveness.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.4204/EPTCS.190.6
Divisions: Faculties > Sciences > School of Computing
Depositing User: Reuben Rowe
Date Deposited: 24 Nov 2017 13:41 UTC
Last Modified: 29 May 2019 19:54 UTC
Resource URI: (The current URI for this page, for reference purposes)
Rowe, Reuben:
  • Depositors only (login required):


Downloads per month over past year