[Agda] Checking termination is not sufficiently exploratory.

[Guillaume Allais]

Hi Serge,

This is how I would do it:

===============================================================
open import Coinduction using (♯_)
import Codata.Musical.Colist as CL
import Codata.Musical.Costring as CS

toMusical : Costring ∞ → CS.Costring
toMusical []       = CL.[]
toMusical (c ∷ cs) = c CL.∷ ♯ toMusical (cs .force)
===============================================================

Note that it's also probably worth replacing my ad-hoc definition of
`Costring` with `Colist Char` where `Colist` comes from `Codata.Colist`.
This way `fromList` and `_++_` are readily available. We also have
`fromMusical` but I see that we are missing `toMusical`. I'll send a PR.

Cheers,
--
gallais



On 06/08/18 18:50, Serge Leblanc wrote:
> Thanks , Guillaume.
> Now, I have a problem to print the result due to the IO functions
> requesting Codata.Musical.Costring.
> I fail to write a function: Costring ∞ → Codata.Musical.Costring
> 
> Dankon, Guillaume.
> Nun, mi havas problemon por afiŝi la resulton pro la IO-funkcioj petas
> Codata.Musical.Costring.
> Mi fiaskas skribi funkcion: Costring ∞ → Codata.Musical.Costring
> 
> Sincere,
> 
> On 2018-08-05 10:24, Guillaume Allais wrote:
>> Hi Serge,
>>
>> Using the new-style codata based on sized types which is available in the
>> latest standard library, you could write something like [see below].
>>
>> Notice the type of `_:++_`: the second argument is a `Thunk` and because
>> the string is non-empty it's fine: we can guarantee it'll be used in a
>> guarded position.
>>
>> Cheers,
>> --
>> gallais
>>
>> ==========================================================================
>> module Costring where
>>
>> open import Size
>> open import Codata.Thunk
>> open import Data.Nat as Nat
>> open import Data.Char
>> open import Data.String hiding (fromList ; _++_ ; _==_)
>> open import Data.List as List hiding (_++_)
>> open import Relation.Nullary.Decidable
>> open import Data.Bool
>> open import Function
>>
>> data Costring (i : Size) : Set where
>>   []  : Costring i
>>   _∷_ : Char → Thunk Costring i → Costring i
>>
>> fromList : List Char → Costring ∞
>> fromList []       = []
>> fromList (x ∷ xs) = x ∷ λ where .force → fromList xs
>>
>> toCostring : String → Costring ∞
>> toCostring = fromList ∘′ toList
>>
>> _++_ : ∀ {i} → Costring i → Costring i → Costring i
>> []       ++ ys = ys
>> (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys
>>
>> _:++_ : ∀ {i} (str : List Char) {_ : False (List.length str Nat.≟ 0)} →
>>        Thunk Costring i → Costring i
>> _:++_ []        {()} xs
>> _:++_ (x ∷ str) {pr} xs = x ∷ λ where .force → fromList str ++ xs .force
>>
>> coSplit″ : ∀ {i} → Costring i → Costring i
>> coSplit″ [] = []
>> coSplit″ (x ∷ xs) with x == '!'
>> ... | false = x ∷ λ where .force → coSplit″ (xs .force)
>> ... | true = toList ">>" :++ λ where .force → coSplit″ (xs .force)
>> ==========================================================================
>>
>> On 03/08/18 20:57, Serge Leblanc wrote:
>>> Would an expert help me to improve the termination checking algorithm?
>>> Does someone already work to improve the algorithm?
>>>
>>> Ĉu spertulo bonvolus helpi min aldoni ŝanĝon al la finiĝokontrola algoritmo?
>>> Ĉu iu jam laboras por plibonigi la algoritmon?
>>>
>>> Sincere
>>>
>>>  
>>> On 2018-07-31 03:02, Serge Leblanc wrote:
>>>> In my opinion, a normal form verification phase could be added without
>>>> changing the termination checking algorithm.
>>>> Laŭ mi, normala kontrola fazo povus esti aldonita sen ŝangi la finiĝan
>>>> kontrolan algoritmon.
>>>>
>>>> Sincere
>>>>
>>>>
>>>> On 2018-07-30 20:06, a.j.rouvoet wrote:
>>>>> I believe that you are right that the two snippets are equivalent,
>>>>> but it requires some computation to show that this is the case.
>>>>> The check that Agda runs on the other hand is very syntactic. This is
>>>>> indeed a limitation, but at least it ensures that checking for
>>>>> termination terminates ;-)
>>>>>
>>>>> On 07/30/2018 06:04 PM, Serge Leblanc wrote:
>>>>>> 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
>>>>>>
>>>>>>
>>>>>> _______________________________________________
>>>>>> 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
>>>
>>>
>>> _______________________________________________
>>> 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
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180806/62904266/attachment.sig>