[Agda] termination proof problem

[Andrea Vezzosi]

Oh, sorry, you are doing this for a particular P where you already
have a bound implemented. I was confused.

On Mon, Mar 28, 2016 at 9:39 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> 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
>>>
>>
>>