Henning Makholm <henning@makholm.net> writes:
> 1. Reducer ethvert fix-udtryk så snart det dukker op i en
> evalueringskontekst.
>
> 2. Reducer *under* fix indtil kroppen er på WHNF; brug
> reduktionsreglen derefter.
Det lyder som forskellen på en eager/strict og en lazy
fixpunktsoperator. Jeg har ikke lige nogen reference, men det kunne
være noget at søge på.
> Intuitivt er det klart for mig at de to strategier har samme
> termineringsegenskaber, hvis altså (2) bliver udvidet med en kunstig
> reduktionsregel
>
> x --> x
>
> således at "fix x.x" diverger som i (1) i stedet for at køre fast, og
> man i øvrigt kun betragter lukkede termer.
Min intutition siger, efter lidt overvejelse, det samme, og beviset
kunne godt blive lidt behåret.
Hvis vi siger at --> er strict reduktion og ==> er lazy, og E[] er
en evaluerings-kontekst, så gælder der
if
fix x.e ==> fix x.E[x]
then
fix x.e --> E'[fix x.e]
(hvor E' er E med (fix x.e) i stedet for x).
Kunne det være at det var nemmere at vise med eksplicitte
evaluerings-kontekster (altså semantikker givet på samme måde som
Felleisens "Syntaktiske Teorier"?).
De to reduktioner ville så have evalueringskontekster, værdier og
reduktioner på formene:
--> :
E ::= [] | E e2| v1 E
v ::= \x.e
E[\x.e v] -> E[e[x|->v]]
E[fix x.e] -> E[e[x|->fix x.e]]
==> :
E ::= [] | E e2 | v1 E | fix x.E
v ::= \x.e
E[\x.e v] -> E[e[x|->v]]
E[fix x.\y.e] -> E[\y.e[x|->fix x.\y.e]]
E[x] -> E[x] (* den kunstige regel der tvinger divergens *)
Jeg ville nok foretrække at droppe den kunstige reduktionsregel, og
kigge på de termer der kører fast i stedet. Jeg tror det er nemmere at
adskille de termer der divergerer naturligt fra dem der divergerer på
grund af den kunstige regel, hvis man lader dem køre fast i stedet.
Der skulle stadig gælde, for programmer der er lukkede lambda-udtryk, at
p -->* v <=> p ==>* v
(hvor --> er den ene reduktionsstrategi og ==> er den anden). Hvis det
resultat er nok, så kan du måske spare noget energi.
Det er selvfølgelig bare skud, da jeg ikke ved hvad du skal bruge det
til :)
> Er ækvivalensen af de to strategier velkendt? Altså, velkendt nok til
> at der er nogen her der kan stange mig en litteraturhenvisning ud, som
> jeg kan stille i stedet for mit eget bevis.
Jeg kender den desværre ikke.
Du er vist på DIKU, så jeg tror du skulle spørge Andrzej Filinski.
Hvis han ikke kan hjælpe, så tror jeg ikke der er mange der kan :)
/L
--
Lasse Reichstein Nielsen - lrn@hotpop.com
Art D'HTML: <URL:
http://www.infimum.dk/HTML/randomArtSplit.html>
'Faith without judgement merely degrades the spirit divine.'