[Agda] termination by contradiction

[Altenkirch Thorsten]

On 01/07/2014 20:40, "Sergei Meshveliani" <mechvel at botik.ru> wrote:

>On 01/07/2014 16:19, Altenkirch Thorsten wrote:
>
>> However, it is not clear how to do symbolic evaluation with MP. That
>> is if we have a hypothetical classical proof of termination this
>> doesn’t tell us wether we can partially execute our program. In the
>> case of a constructive proof this is the case.
>>
>> We could say that we can run the program if the proof is closed but
>> this seems a bit weird.
>
>Consider the example:
>
>  findNatByContra :
>           (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P
> 
>  findNatByContra P P? _ =  findFrom 0
>    where
>    findFrom : ℕ → Σ ℕ P
>    findFrom n = case P? n of \ { (yes Pn) → (n , Pn)
>                                ; (no _)   → findFrom (suc n) }
>
>Assuming Markov's rule, we consider the type
>                                ¬ (∀ n → ¬ P n) → (\exist \n → P n)
>as inhabited,
>and this proves that  findFrom  is terminating.
>Right?

Markov’s rule tells us that we can prove termination classically.

>
>> if we have a hypothetical classical proof of termination this
>> doesn’t tell us wether we can partially execute our program. In the
>> case of a constructive proof this is the case.
>
>Do you consider the termination proof by
>                                    ¬ (∀ n → ¬ P n) → (\exist \n → P n)
>as constructive?

Not sure I understand the question.

>Can we partially execute the program  findFrom ?
>(why do you add `partially' ?).

In Agda we need to execute programs with variables. This is usually called
symbolic evaluation. It is important that symbolic evaluation terminates
otherwise the type checker will hang.

In Agda every recursive program can be computed until it gets stuck.
However, it is not clear what this means for findFrom. If we recursively
unfold findFrom evaluation will not terminate.

I guess you have an operational semantics in mind which does not unfold
under the case. While this seems reasonable (and solves the problem) it is
not without problems.

Thorsten


>
>Thanks,
>
>------
>Sergei
>
>