/ Forside / Karriere / Uddannelse / Højere uddannelser / Nyhedsindlæg
Login
Glemt dit kodeord?
Brugernavn

Kodeord


Reklame
Top 10 brugere
Højere uddannelser
#NavnPoint
Nordsted1 1588
erling_l 1224
ans 1150
dova 895
gert_h 800
molokyle 661
berpox 610
creamygirl 610
3773 570
10  jomfruane 570
Lambdakalkyle
Fra : Henning Makholm


Dato : 05-03-03 00:03

Der plejer at være en del dataloger her:

Jeg har en lambdakalkyle med en fixpunktoperator

e ::= ... | fix x.e

og en tilhørende beta"reduktion"

fix x.e --> e[x->fix x.e]

Jeg har to reduktionsstrategier for fix, som begge to skal passe ind i
almindelig call-by-value:

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.

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. Jeg mener også jeg kan
bevise at dette er tilfældet, men det bliver forholdsvis teknisk og
kommer til at stjæle opmærksomheden fra det jeg egentlig er ved at
skrive.

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.

--
Henning Makholm "De kan rejse hid og did i verden nok så flot
Og er helt fortrolig med alverdens militær"

 
 
Lasse Reichstein Nie~ (05-03-2003)
Kommentar
Fra : Lasse Reichstein Nie~


Dato : 05-03-03 01:27

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.'

Henning Makholm (05-03-2003)
Kommentar
Fra : Henning Makholm


Dato : 05-03-03 21:49

Scripsit Lasse Reichstein Nielsen <lrn@hotpop.com>

> 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 :)

Hm, det kunne jeg måske godt selv have fundet på - han sidder bag
døren overfor min. :) Men det var din henvisning der fik mig til
faktisk at gøre det, så tak for hjælpen. Vi fandt en helt tredje
løsning (som er specifik for den sammenhæng jeg skulle bruge beviset i).

--
Henning Makholm "However, the fact that the utterance by
Epimenides of that false sentence could imply the
existence of some Cretan who is not a liar is rather unsettling."

Søg
Reklame
Statistik
Spørgsmål : 177552
Tips : 31968
Nyheder : 719565
Indlæg : 6408849
Brugere : 218887

Månedens bedste
Årets bedste
Sidste års bedste