[Agda] Re: Logical meaning of nontermination

[Samuel Gélineau]

>> Can we regard the following function as proof? Can we read it as
>> conversion of statement ((P→⊥)→⊥) to ((⊥→⊥)→⊥) with last ⊥ encoded by
>> nontermination?
>
> Yes, but in an inconsistent logic.

I don't think that's quite right. The function ⊥⊥→⊥converts
proposition ((P→⊥)→⊥) to proposition (P→⊥), so it proves ((P→⊥)→⊥) →
P→⊥) in an inconsistent logic. But the question isn't whether a
non-terminating function of type Q is still a proof of proposition Q,
but whether that function is a proof of (Q →⊥) instead. At least,
that's what I think the question is. ((⊥→⊥)→⊥) is a typo for
((P→⊥)→⊥), isn't it?


The logical meaning of a program is its Curry-Howard interpretation.
And that interpretation is performed by type-checking the term, and
converting each type-checking step into an inference rule. Since
non-terminating functions still type-check, I think it makes a lot of
sense to ask why non-terminating programs shouldn't count as proofs.

And the answer has to do with scoping rules. When a variable of type Q
is in scope, it means that we can use that fact at this point of the
proof. When we use let expressions or previously-written programs,
then we can use those facts with confidence, since we just proved
them. But when we write a recursive function, we cheat by assuming
proposition Q and using that assumption to prove Q! No wonder, then,
that recursion allows us to prove any proposition whatsoever,
including Q and ¬Q. That is, no wonder that unrestricted recursion
makes the corresponding logic inconsistent.


But again, that's not the question which was originally asked. We know
that we can't interpret a non-terminating program of type Q as a proof
of proposition Q, but could we somehow interpret it as a proof of
something else, like (Q →⊥), or more generally (NonT Q) for some
proposition transformer NonT?

Well, first of all, you need to be careful about what you mean by
non-termination. Do you mean that the program has been checked not to
terminate? On all inputs? Some inputs? Or has termination-checking
simply failed to show that the program terminates on all inputs? I
think the simplest is to go with unrestricted recursion. (NonT Q)
shall be the type of programs which assume Q in order to conclude Q:

NonT Q = Q → Q

With such a definition, it is clear that (NonT Q) is inhabited for all
propositions Q. And that's fine, since non-termination does allow you
to write a program of type Q for any type Q. But that makes the proofs
very useless. Sure, you can chose to interpret a non-terminating proof
of Q as a proof of (Q → Q), but what are you going to do with that
knowledge? You knew that the proposition was true already, without
using non-termination. Are there other, more useful interpretations?

Vag wants (I think) to interpret (NonT Q) as (Q →⊥), but doing so
isn't wise. Values of type (Q →⊥) have a specific meaning in agda: it
means that Q cannot be proven. But since non-termination allows you to
write programs with any type Q, this interpretation tells you that (Q
→⊥) is inhabited for all propositions Q, and thus that no Q can be
proven! Take any Q which actually can be proven (say, Nat → Nat), and
you have a contradiction, i.e., an inconsistent logic.

So... after much deliberation, I do second Nils in his answer, even
though I'm not sure he answered the right question. You can interpret
a non-terminating proof of Q as a proof of (Q →⊥), but as Nils said,
that gives you an inconsistent logic.

– Samuel