[Agda] termination proof problem

[Andrea Vezzosi]

On Mon, Mar 28, 2016 at 8:47 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> No.
> The problem is
>
>   Having certain   P : ℕ → Set,  P? : Decidable P,   and any  n : ℕ,
>
>   find the first  y  after  n  such that  P y.
>
> That is one needs to implement in Agda
>
>      search :  (n : ℕ) →  ∃ \y →  n < y  ×  P y  ×  IsMinimalSuch y

What if "P y" never holds?

>
> And it is already type-checked the program for
>
>      bound :  (n : ℕ) →  ∃ \y →  n < y  ×  P y
>
> Having this `bound', I program a linear search-through for `search',
> where `bound' serves as a counter to prove termination.
>
> The functions for  P, P?, bound   are simple to type check.
> Also P and P' are fast at run-time, assume that they take one tick of
> time.
> But `bound'  is expensive at run-time.
> For example, to computing  (bound 50)  makes a linear search-through
> practically unusable -- if it ever applies (bound 50) at run-time.
>
> Concerning all the rest -- see my first letter on the subject.
>
> Being not an expert in constructive mathematics, I understand the case
> as follows:
>
> ------------------------------------------------
> It is given a terminating algorithm for `bound'. In a linear
> search-through with  y = n+1, n+2 ...,  with checking each (P? y),
> the event of (P y) will happen not later than  y = bound n.
> Hence this search-through is proved terminating.
> Hence there is no need to compare  y  to  (bound n) for each current  y
> at the run-time computation.
> One only has to check (P? y). If (yes _), the search stops, otherwise go
> to (suc y).
> ------------------------------------------------
>
> How to express a similar approach in Agda?
> In my attempts, the program applies for each  y  the comparison
> ((bound n) - y)  to  0,  and even a single such comparison spoils
> performance when it happens at run-time.
>
> Thanks,
>
> ------
> Sergei
>
>
> On Mon, 2016-03-28 at 18:37 +0900, Andrea Vezzosi wrote:
>> Do you also mean "y < n" ?
>>
>> On Mon, Mar 28, 2016 at 5:01 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
>> > On Sun, 2016-03-27 at 23:56 +0400, Sergei Meshveliani wrote:
>> >> Can people explain, please, the following subject concerning termination
>> >> proof tools?
>> >>
>> >> Having certain
>> >>                    P : ℕ → Set  and   P? : Decidable P,
>> >>
>> >> one needs to implement
>> >>
>> >>     search :  (n : ℕ) → ∃ \y →  m < y × P y × IsMinimalSuch y
>> >>
>> >> -- find the first  y  after  m  such that  P y.
>> >> [..]
>> >
>> >
>> > Fixing a typo:  replace  "m"  with  "n"  in these two lines.
>> >
>> []
>
>
>
>
>> > ------
>> > Sergei
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>