[TYPES] What's a program? (Seriously)

[Martin Escardo]

On 18/05/2021 22:18, Talia Ringer wrote:
> Do programs need to have
> realizable inputs?

That's an excellent question.

You should check the book

"Higher-Order Computability" by John Longley and Dag Normann (Springer
2015). https://www.springer.com/gp/book/9783662479919

In the 1950's people asked this question to themselves (Kleene, Kreisel
and others).

The answer is that there are two classical theories of higher-order
computability.

  * computable data and computable functions.
  * continuous data and computable functions.

Technically, they amount to realizability over K1 (Hyland's "effective
topos") and realizability over K2 (Kleene-Vesley topos), where K1 and K2
are Kleene's first and second combinatory algebras.

Other proposals where given, but all of them turned out to be (with hard
work) equivalent to K1 or K2.

These two theories don't agree. All they agree about is what functions
N->N are or are not computable (and they agree with Turing). But e.g.
they don't agree regarding what functions (N->N)->N are allowed and
which ones are computable.

The difference is what you say: do we consider computable functions over
arbitrary inputs, or just over computable inputs?

The precise answers are technically subtle (and mathematically
interesting).

>     To my knowledge, a proof is a very (very) specific kind of program.
> 
> 
>  What makes it more specific? In my mind, you can certainly view any
> program in any language as a proof in some logical system, even if the
> logical system is not actually implemented as the language's type
> checker, and even if the corresponding logic is unsound. A proof in an
> unsound logic is still a proof, I think---just a possibly useless one
> (possibly useful, though, since you can have incorrect assumptions and
> still sometimes prove things that in no way rely on them).

I am not sure I understand this, but I would be willing to discuss it to
clarify it.

Best,
Martin