© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Publications by Prof David Turner
Also view these in the Kent Academic Repository
Articles
Turner, D. A. (2021) 'Constructive mathematics, Church's Thesis, and free choice sequences', Lecture Notes in Computer Science. 17th Conference on Computability in Europe, CiE 2021, Springer. doi: 10.1007/978-3-030-80049-9_44.
Abstract | View in KAR | View Full Text
We see the defining properties of constructive mathematics as being the proof interpretation of the logical connectives and the definition of function as rule or method. We sketch the development of intuitionist type theory as an alternative to set theory. We note that the axiom of choice is constructively valid for types, but not for sets. We see the theory of types, in which proofs are directly algorithmic, as a more natural setting for constructive mathematics than set theories like IZF. Church's thesis provides an objective definition of effective computability. It cannot be proved mathematically because it is a conjecture about what kinds of mechanisms are physically possible, for which we have scientific evidence but not proof. We consider the idea of free choice sequences and argue that they do not undermine Church's Thesis.
Turner, D. A. (2013) 'Some History of Functional Programming Languages', Lecture Notes in Computer Science. Edited by H.-W. Loidl and R. Peña. Springer, pp. 1-20. doi: 10.1007/978-3-642-40447-4_1.
Abstract | View in KAR | View Full Text
We study a series of milestones leading to the emergence of lazy, higher order, polymorphically typed, purely functional programming languages. An invited lecture given at TFP12, St Andrews University, 12 June 2012.
Turner, D. A. (2004) 'Total Functional Programming', Journal of Universal Computer Science, pp. 751-768. doi: 10.3217/jucs-010-07-0751.
The driving idea of functional programming is to make programming more closely related to mathematics. A program in a functional language such as Haskell or Miranda consists of equations which are both computation rules and a basis for simple algebraic reasoning about the functions and data structures they define. The existing model of functional programming, although elegant and powerful, is compromised to a greater extent than is commonly recognised by the presence of partial functions. We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. Among other things this requires a type distinction between data, which is finite, and codata, which is potentially infinite.
Telford, A. J. and Turner, D. A. (2000) 'Ensuring Termination in ESFP', Journal of Universal Computer Science. 15th British Colloquium in Theoretical Computer Science, Keele, pp. 474-488. doi: 10.3217/jucs-006-04.
In previous papers we have proposed an elementary discipline of strong functional programming (ESFP), in which all computations terminate. A key feature of the discipline is that we introduce a type distinction between data which is known to be finite, and codata which is (potentially) infinite. To ensure termination, recursion over data must be well-founded, and corecursion (the definition schema for codata) must be productive, and both of these restrictions must be enforced automatically by the compiler. In our previous work we used abstract interpretation to establish the productivity of corecursive definitions in an elementary strong functional language. We show here that similar ideas can be applied in the dual case to check whether recursive function definitions are strongly normalising. We thus exhibit a powerful termination analysis technique which we demonstrate can be extended to partial functions.
Turner, D. A. (1995) 'Elementary strong functional programming', Functional Programming Languages in Education. Edited by P. H. Hartel and R. Plasmeijer. 1st International Symposium on Functional Programming Languages in Education (FPLE 95), Berlin, Germany: Springer, pp. 1-13. doi: 10.1007/3-540-60675-0_35.
Abstract | View in KAR | View Full Text
Functional programming is a good idea, but we haven't got it quite right yet. What we have been doing up to now is weak (or partial) functional programming. What we should be doing is strong (or total) functional programming - in which all computations terminate. We propose an elementary discipline of strong functional programming. A key feature of the discipline is that we introduce a type distinction between data, which is known to be finite, and codata, which is (potentially) infinite.
Book sections
Turner, D. A. (2006) 'Church's Thesis and Functional Programming', in Olszewski, A., Woleński, J., and Janusz, R. (eds) Church's Thesis After 70 Years. Berlin: Ontos Verlag, pp. 518-544. doi: 10.1515/9783110325461.
Abstract | View in KAR | View Full Text
David Turner's contribution to a volume published on the 70th anniversary of Church's Thesis. ERRATUM: In the published version (Ontos Verlag 2006) Wadsworth's 1976 result on Solvability and head normal form (p6 bottom) was incorrectly attributed to Böhm - this has now been corrected.
Telford, A. J. and Turner, D. A. (1997) 'Ensuring Streams Flow', in Johnson, M. (ed.) Algebraic Methodology and Software Technology 6th International Conference. Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney Australia, December 1997, Berlin, Germany: Springer, pp. 509-523. doi: 10.1007/BFb0000493.
Abstract | View in KAR | View Full Text
It is our aim to produce an elementary strong functional programming (ESFP) system. To be useful, ESFP should include structures such as streams which can be computationally unwound infinitely often. We describe a syntactic analysis to ensure that infinitely proceeding structures, which we shall term codata , are productive. This analysis is an extension of the check for guardedness that has been used with definitions over coinductive types in Martin-Lof's type theory and in the calculus of constructions. Our analysis is presented as a form of abstract interpretation that allows a wider syntactic class of corecursive definitions to be recognised as productive than in previous work. Thus programmers will have fewer restrictions on their use of infinite streams within a strongly normalizing functional language.
Monographs
Telford, A. J. and Turner, D. A. (2000) A Hierarchy of Languages with Strong Termination Properties. University of Kent.
Abstract | View in KAR | View Full Text
In previous papers we have proposed an elementary discipline of strong functional programming (ESFP), in which all computations terminate. A key feature of the discipline is that we introduce a type distinction between data which is known to be finite, and codata which is (potentially) infinite. To ensure termination, recursion over data must be well-founded, and corecursion (the definition schema for codata) must be productive, and both of these restrictions must be enforced automatically by the compiler. In our previous work we used abstract interpretation to establish the productivity of corecursive definitions in an elementary strong functional language. We show here that similar ideas can be applied in the dual case to check whether recursive function definitions are strongly normalising. We thus exhibit a powerful termination analysis technique which we demonstrate can be extended to partial functions.
Telford, A. J. and Turner, D. A. (1997) Ensuring the Productivity of Infinite Structures. University of Kent.
Abstract | View in KAR | View Full Text
It is our aim to produce an elementary strong functional programming (ESFP) system. To be useful, ESFP should include structures such as streams which can be computationally unwound infinitely often. We describe a syntactic analysis to ensure that infinitely proceeding structures, which we shall term codata , are productive. This analysis is an extension of the check for guardedness that has been used with definitions over coinductive types in Martin-Lof's type theory and in the calculus of constructions. Our analysis is presented as a form of abstract interpretation that allows a wider syntactic class of corecursive definitions to be recognised as productive than in previous work. Thus programmers will have fewer restrictions on their use of infinite streams within a strongly normalizing functional language.