Confusion in the Church-Turing Thesis

TL;DR

This paper clarifies misconceptions about the Church-Turing Thesis by distinguishing between numerical and symbolic computations, showing that certain models like SF-calculus align with Turing computability and impact language design.

Contribution

It demonstrates that the SF-calculus can define equality of normal forms, establishing a model equivalent to Turing computability, unlike some lambda-models.

Findings

SF-calculus defines equality of closed normal forms

Models like lambda-models may not be Turing-equivalent

Implications for programming language design

Abstract

The Church-Turing Thesis confuses numerical computations with symbolic computations. In particular, any model of computability in which equality is not definable, such as the lambda-models underpinning higher-order programming languages, is not equivalent to the Turing model. However, a modern combinatory calculus, the SF-calculus, can define equality of its closed normal forms, and so yields a model of computability that is equivalent to the Turing model. This has profound implications for programming language design.