[CakeML-dev] Pathological modLang programs

[Yong Kiam]

Oh, I thought this was only a property of type-correct programs (replace
0,1,2 with x y z in my example), but looking at source-to-mod, it appears
that it should be provable if next_global starts at 0. Thanks!

On Sun, Mar 26, 2017 at 1:23 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> I like the 3rd approach you mention. Rather than checking that property
> within mod_live, I think you could prove it as a syntactic property of
> source_to_mod. (This puts in the same category of other syntactic
> properties that are required for later phases and proved to be propagated
> by earlier ones.) It sounds like a reasonably simple property to deal with.
>
> On 26 March 2017 at 13:09, Yong Kiam <tanyongkiam at gmail.com> wrote:
>
>> Hi dev,
>>
>> I've been stuck on mod_live for awhile, the main problem seems to be that
>> this is a legitimate modLang program:
>>
>> val 0 = fn () => Global 1
>> val 1 = ...
>> val 2 = (Global 0) ()
>> ... Global 1 never read here ...
>>
>> In my current set up, I pass a set of live globals from back to front
>> through the list of decs, tracking all the globals that could have been
>> read.
>>
>> In the above fragment, this approach would delete the val 1 = ... line
>> because it was never read from back to front. I think only focusing on
>> deleting Dletrecs does not solve the problem either.
>>
>> I have two ways around this:
>>
>> 1) fallback to a more naive analysis, i.e. walk through all the
>> declarations and keep every global that is ever read. This would not be
>> able to catch chains of dead globals:
>>
>> val 0 = ...
>> val 1 = Global 0
>> val 2 = Global 1
>> ... (0,1,2 all dead, but only 2 would be removed)
>>
>> 2) go to a more complicated one. Not only do I go back to front, but I
>> also go front to back and track for each global, the set of globals that it
>> can transitively reference. When a global gets added, this analysis would
>> have to add all the globals that can be transitively read via that global.
>> (so when 0 gets added above, it transitively adds 1).
>>
>> I didn't particularly like 1 or 2 because 1) seems too naive and 2) seems
>> to difficult (having to deal with termination of the transitive addition).
>>
>> A potential 3rd approach is to essentially type check the entire program
>> and only apply the removal [ass if all the globals happen to point in the
>> right way. i.e. any dec at position n must only mention globals < n. I
>> think that still works in modLang before any complicated knot tying is done.
>>
>> Does anyone have better suggestions? Or am I missing something important?
>>
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170326/dda33f84/attachment.html>