[Agda] Checking termination is not sufficiently exploratory.

[Serge Leblanc]

Yes, but you translat the code (toCostring ">>") ++ coSplit "(♭ xs) to
its normal form, it equals to '>' ∷ ♯ ('>' ∷ ♯ coSplit '(♭ xs)). Right?
So, the recursive call is well protected by a constructor.

Jes, sed vi plenumas la kodon (toCostring ">>") ++ coSplit″ (♭ xs) ĝis
sia normala formo, ĝi egalas al  '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs)). Ĉu ne ?
Do, la memsinkceva alvoko estas bone ŝirmi per konstruisto.

On 2018-07-30 16:59, a.j.rouvoet wrote:
>
> For coSplit to pass the checker, the recursive invocation must appear
> guarded by a constructor.
> This is clearly the case in coSplit', but not necessarily in coSplit''
> (e.g. when toString ">>" returns the empty costring).
>
>
> On 07/30/2018 04:55 PM, Serge Leblanc wrote:
>> Dear all,
>> Why the checking termination rejects the coSplit" function although
>> the coSplit' function is accepted ?
>> Why the checking termination so suspicious?
>> Sincerely
>>
>> Estimataj ĉiuj,
>> Kial la finiĝa kontrolo malakceptas la funkcion coSplit″ kvankam la
>> funkcio coSplit′ trafas ?
>> Kial la finiĝa kontrolo estas tiel malakceptanda ?
>> Sincere
>>
>>   coSplit′ : Costring → Costring
>>   coSplit′ [] = []
>>   coSplit′ (x ∷ xs) with x ≐ '!'
>>   ... | false = x ∷ ♯ coSplit′ (♭ xs)
>>   ... | true = '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs))
>>
>>   coSplit″ : Costring → Costring
>>   coSplit″ [] = []
>>   coSplit″ (x ∷ xs) with x ≐ '!'
>>   ... | false = x ∷ ♯ coSplit″ (♭ xs)
>>   ... | true = (toCostring ">>") ++ coSplit″ (♭ xs)
>>
>>   main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘ coSplit′) s
>>
>> -- 
>> Serge Leblanc
>> ------------------------------------------------------------------------
>> gpg --search-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180730/e1742cb4/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 195 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180730/e1742cb4/attachment.sig>