Computing with internal structure

Abstract:

The Church-Turing Thesis asserts that all computable, numerical functions can be computed using either the lambda-calculus of functions or a Turing Machine with its state and tape. The thesis extends to arbitrary computation since Goedelisation can encode any language into numbers. Such an encoding, or compilation, creates a gap between the source language and the target language so it is more interesting to seek representations of one language within another. For example, the operators S and K of combinatory logic can be represented as lambda-abstractions, and conversely. For this reason, SK-logic is said to be combinatorially complete. However, contrary to the common understanding of the past 70 years, it turns out that there are simple combinatory logics that cannot be expressed within SK-logic, e.g. our SF-logic [1].

This talk will begin with an overview of the classical theory of computation mentioned above, with an emphasis on equational reasoning in SK-logic. Then SF-logic will be introduced, and proven to be more expressive than SK-logic. In particular, it supports computation by (syntactic) pattern matching, as developed in pattern calculus [2] and implemented in the bondi programming language [3].