1 Eine rationale Dekonstruktion von Landin’s SECD-Maschine Betreuerin: Prof. Dr. Rita Loogen...

1

Eine rationale Dekonstruktion von Landin’s SECD-Maschine

Betreuerin: Prof. Dr. Rita Loogen

Bearbeiter: Dong Liang

2

Übersicht

Einführung von SECD MachineEinleitung Struktur der SECD machineVorbedingungen und Gebiet der Darlegung

Dekonstruktion von der SECD MachineDie originale SECD MachineEine strukturiertere SpezifikationHöhere OrdnungOhne Dump-FortsetzungOhne Control-FortsetzungOhne Stack

Fazit

3

1.1Einleitung SECD-Maschine war die erste Abstrakte Maschine für dasλ-kalkül Die Richtung für die weitere Entwicklung der abstrakten Maschinen Und für die Sprachen der funktionalen Programmierung Dekonstruktion der SECD-Maschine in λ- Interpret d.h. eine

Auswertungsfunktion Bauen λ-interpreten in eine SECD-maschine wieder auf Bestandteile der SECD-Maschine

Stack Umgebung Control Dump

4

1.2 Struktur der SECD machine

Die SECD-machine ist als eine Transitionsfunktion definiert.

run : S * E* C * D -> value

Vier Komponenten der SECD-Machin

Ein Stack für Zwischenwerte mit Typ S Eine Umgebung mit Typ E Ein Control-Stack mit Typ C Ein Dump mit Typ D

5

1.3 Vorbedingungen und Gebiet der Darlegung(1) Die Ausgangssprache : λ-kalkül structure Source = struct type ide = string datatype term = LIT of int c | VAR of ide x | LAM of ide * term λx.t | APP of term * term (t t‘) type program = term end

Term = c | x | λx.t | (t t‘)

β-Reduktionsregel (λx.t t‘ ) β t[x | t‘ ]

Bsp: (x. (succ“x“) 5 )

6

1.3 Vorbedingungen und Gebiet der Darlegung(2) Die (polymorph) Umgebung: Env signature ENV = sig type ’a env val empty : ’a env val extend : Source.ide * ’a * ’a env -> ’a env val lookup : Source.ide * ’a env -> ’a end

Das leere Umgebung wird von Env.empty bezeichnet. Die Funktion, die eine Umgebung mit einer neuen Bindung erweitert,

wird mit Env.extend bezeichnet. Die Funktion, die den Wert eines Bezeichners von einem Umgebung holt,

wird mit Env.lookup bezeichnet.

7

1.3 Vorbedingungen und Gebiet der Darlegung(3) Das Wertbreich der λ-kalkül : Interger ; successor function ; function closure

datatype value = INT of int | SUCC | CLOSURE of value Env.env * Source.ide * Source.term

Die initiale Umgebung val e_init = Env.extend ("succ", SUCC, Env.empty)

8

2.Dekonstruktion von der SECD Machine

2.1 Die originale SECD Machine2.2 Eine strukturiertere Spezifikation Vergleichen von originale SECD Machine und strukrtuiertere Spezifikation2.3 Höhere Ordnung Vergleichen von struktuiertere Spezifikation und höherer Ordnung2.4 Ohne Dump-Fortsetzung Vergleichen von höherer Ordnung und ohne Dump-Fortsetzung2.5 Ohne Control-Fortsetzung Vergleichen von ohne Dump-Fortsetzung und ohne Control-Fortsetzung 2.6 Ohne Stack Vergleichen von ohne Control-Fortsetzung und ohne Stack

9

2.1 Die originale SECD machine(1) Die SECD-Maschine wird mit Übergängen zwischen seinen vier Komponenten

definiert Die vier Komponenten der originale SECD machine

Stack_register enthält ein list von Zwischenresultate value list Environment_ register enthält ein list von Umgebung value Env.env control_ register enthält control directives Directive datatype directive = TERM of Source.term | APPLY Dump_ register enthält Liste von Dreiergruppen. (value list * value Env.env * directive list) list

10

2.1 Die originale SECD machine(2)

Die originale SECD Machine

(* run : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = directive list *) (* D = (S * E * C) list *)

(* evaluate 0 : Source.program -> value *) fun evaluate0 t = run (nil, e_init, (TERM t) :: nil, nil)

11

2.1 Die originale SECD machine(3)

fun run (v :: nil, e’, nil, nil) (* 1 *) = v | run (v :: nil, e’, nil, (s, e, c) :: d) (* 2 *) = run (v :: s, e, c, d) | run (s, e, (TERM (LIT n)) :: c, d) (* 3 *) = run ((INT n) :: s, e, c, d) | run (s, e, (TERM (VAR x)) :: c, d) (* 4 *) = run ((Env.lookup (x, e)) :: s, e, c, d) | run (s, e, (TERM (LAM (x, t))) :: c, d) (* 5 *) = run ((CLOSURE (e, x, t)) :: s, e, c, d) | run (s, e, (TERM (APP (t0, t1))) :: c, d) (* 6 *) = run (s, e, (TERM t1) :: (TERM t0) :: APPLY :: c, d) | run (SUCC :: (INT n) :: s, e, APPLY :: c, d) (* 7 *) = run ((INT (n+1)) :: s, e, c, d) | run ((CLOSURE (e’, x, t)) :: v’ :: s, e, APPLY :: c, d) (* 8 *) = run (nil, Env.extend (x, v’, e’), (TERM t) :: nil, (s, e, c) :: d)

12

2.2 Eine strukturiertere Spezifikation(1) In der Definition von Abschnitt 2,1, werden alle möglichen Übergänge

zusammen in einer rekursiven Funktion run definiert. Faktorisiere run in einige gegenseitig rekursive Funktionen, davon

jede mit einer Induktionsvariable.

run_c interpretiert die list von control run_d interpretiert das Dump run_t interpretiert das erste Term in die list von Control run_a interpretiert der erste Resultat in Stack

13

2.2 Eine strukturiertere Spezifikation(2) Diese Transitionsfunktion ist schwierig Es ist in vier Transitionsfunktion verteilt jede hat eine Induktionsvariable

run_c : S * E * C * D -> value run_d : S * D -> value run_t : term * S * E * C * D -> value run_a : S * E * C * D -> value

run_c: Algemaine Übergangsfunktion run_d: Wenn Control_stack leer ist run_t: Wenn Control_stack ein Term enthält Run_a:Wenn Control_stack ein Applikation enthält

14

Vergleichen von der originale SECD Machine und der stukturiertere Spezifikation

Dadurch wird die SECD-Machine wie folgende definiert:

Die originale SECD Machine

(* run : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = directive list *) (* D = (S * E * C) list *)

(* evaluate 0 : Source.program -> value *) fun evaluate0 t = run (nil, e_init, (TERM t) :: nil, nil)

Die stukturiertere SECD Machine

(* run_c : S * E * C * D -> value *) (* run_d : S * D -> value *) (* run_t : Source.term * S * E * C * D -> value *) (* run_a : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = directive list *) (* D = (S * E * C) list *)

(* evaluate 1 : Source.program -> value *) fun evaluate1 t = run_t (t, nil, e_init, nil, nil)

15


Das originale Fall

fun run (v :: nil, e’, nil, nil)

= v | run (v :: nil, e’, nil, (s, e, c) :: d)

= run (v :: s, e, c, d)

Die strukturiertere Spezifikation

fun run_c (s, e, nil, d) = run_d (s, d) | run_c (s, e, (TERM t) :: c, d) = run_t (t, s, e, c, d) | run_c (s, e, APPLY :: c, d) = run_a (s, e, c, d) and run_d (v :: nil, nil) = v | run_d (v :: nil, (s, e, c) :: d) = run_c (v :: s, e, c, d)

16


| run (s, e, (TERM (LIT n)) :: c, d)

= run ((INT n) :: s, e, c, d)

| run (s, e, (TERM (VAR x)) :: c, d)

= run ((Env.lookup (x, e)) :: s, e, c, d)

| run (s, e, (TERM (LAM (x, t))) :: c, d) = run ((CLOSURE (e, x, t)) :: s, e, c, d)

| run (s, e, (TERM (APP (t0, t1))) :: c, d)

= run (s, e, (TERM t1) :: (TERM t0) :: APPLY :: c, d)

and run_t (LIT n, s, e, c, d) = run_c ((INT n) :: s, e, c, d) | run_t (VAR x, s, e, c, d) = run_c ((Env.lookup (x, e)) :: s, e, c, d) | run_t (LAM (x, t), s, e, c, d) = run_c ((CLOSURE (e, x, t)) :: s, e,c, d) | run_t (APP (t0, t1), s, e, c, d) = run_t (t1, s, e, (TERM t0) :: APPLY :: c, d)

17


run (SUCC :: (INT n) :: s, e, APPLY :: c, d) = run ((INT (n+1)) :: s, e, c, d)

| run ((CLOSURE (e’, x, t)) :: v’ :: s, e, APPLY :: c, d) = run (nil, Env.extend (x, v’, e’), (TERM t) :: nil, (s, e, c) :: d)

Proposition 1: Die Quellenprogrammen evaluate0 und

Resultat

and run_a (SUCC :: (INT n) :: s, e, c, d) = run_c ((INT (n+1)) :: s, e, c, d) | run_a ((CLOSURE (e’, x, t)) :: v’ :: s, e, c, d) = run_t (t, nil, Env.extend (x, v’, e’), nil, (s, e, c) :: d)

evaluate1 erbringen das gleiche

18

2.3 Höhere Ordnung (1)

In Abschnitt 2.2, gibt es zwei Möglichkeiten um ein Dump zu konstruieren (Nil und Cons)

und drei Möglichkeiten um eine Liste von Control zu konstruieren(nil, a term, and apply directive).

In höherer Ordnung definiert das Dump und Control als Fortsetzung

(* run_t : Source.term * S * E * C * D -> value *) (* run_a : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = (S * E * D) -> value *) (* D = S -> value *)

19

Vergleichen von strukturierterer Spezifikation und der höherer Ordnung

Die stukturiertere SECD Machine

(* run_c : S * E * C * D -> value *) (* run_d : S * D -> value *) (* run_t : Source.term * S * E * C * D -> value *) (* run_a : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = directive list *) (* D = (S * E * C) list *)

(* evaluate 1 : Source.program -> value *) fun evaluate1 t = run_t (t, nil, e_init, nil, nil)

fun run_c (s, e, nil, d) = run_d (s, d) | run_c (s, e, (TERM t) :: c, d) = run_t (t, s, e, c, d) | run_c (s, e, APPLY :: c, d) = run_a (s, e, c, d) and run_d (v :: nil, nil) = v | run_d (v :: nil, (s, e, c) :: d) = run_c (v :: s, e, c, d)

Die höhere Ordnung (* run_t : Source.term * S * E * C * D -> value *) (* run_a : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = (S * E * D) -> value *) (* D = S -> value *)

(* evaluate2 : Source.program -> value *) fun evaluate2 t = run_t (t, nil, e_init, fn (s, _ , d) => d s, fn (v :: nil) => v)

20


Die strukturiertere Spezifikation

run_t (LIT n, s, e, c, d) = run_c ((INT n) :: s, e, c, d) | run_t (VAR x, s, e, c, d) = run_c ((Env.lookup (x, e)) :: s, e, c, d) | run_t (LAM (x, t), s, e, c, d) = run_c ((CLOSURE (e, x, t)) :: s, e, c, d) | run_t (APP (t0, t1), s, e, c, d) = run_t (t1, s, e, (TERM t0) :: APPLY :: c, d)

Die höhere Ordnung

fun run_t (LIT n, s, e, c, d) = c ((INT n) :: s, e, d) | run_t (VAR x, s, e, c, d) = c ((Env.lookup (x, e)) :: s, e, d) | run_t (LAM (x, t), s, e, c, d) = c ((CLOSURE (e, x, t)) :: s, e, d) | run_t (APP (t0, t1), s, e, c, d) = run_t (t1, s, e, fn (s, e, d) => run_t (t0, s, e, fn (s, e, d) => run_a (s, e, c, d), d), d)

21


run_a (SUCC :: (INT n) :: s, e, c, d) = run_c ((INT (n+1)) :: s, e, c, d) | run_a ((CLOSURE (e’, x, t)) :: v’ :: s, e, c, d) = run_t (t, nil, Env.extend (x, v’, e’), nil, (s, e, c) :: d)

Proposition 2: Die Quellenprogrammen gleiche Resutat

run_a (SUCC :: (INT n) :: s, e, c, d) = c ((INT (n+1)) :: s, e, d)‚ | run_a ((CLOSURE (e’, x, t)) :: v’ :: s, e, c, d) = run_t (t, nil, Env.extend (x, v’, e’), fn (s, _, d) => d s, fn (v :: nil) => c (v :: s, e, d))

evaluate1 und evaluate2 erbringen Sie das

22

2.4 Ohne dump-Fortsetzung Die Version von Abschnitt 2.3 arbeitet mit Fortsetzungsfunktionen

(continuation-passing-style). Jetzt: Elimination der dump-Fortsetzungsfunktion Benennen run_t als eval und run_a als apply um.

(* eval : Source.term * S * E * C -> stack *) (* apply : S * E * C -> S *) (* where S = value list *) (* E = value Env.env *) (* C = S * E -> S *)

23

Vergleichen von höherer Ordnung und ohne dump-Fortsetzung

Die höhere Ordnung (* run_t : Source.term * S * E * C * D -> value *) (* run_a : S * E * C * D -> value *) (* where S = value list *) (* E = value Env.env *) (* C = (S * E * D) -> value *) (* D = S -> value *)

(* evaluate2 : Source.program -> value *) fun evaluate2 t = run_t (t, nil, e_init, fn (s, _ , d) => d s, fn (v :: nil) => v)

Ohne Dump-Fortsetzung


(* evaluate3 : Source.program -> value *) fun evaluate3 t = let val (v :: nil) = eval (t, nil, e_init, fn (s, _ ) => s) in v end

24


Die höhere Ordnung

fun run_t (LIT n, s, e, c, d) = c ((INT n) :: s, e, d) | run_t (VAR x, s, e, c, d) = c ((Env.lookup (x, e)) :: s, e, d) | run_t (LAM (x, t), s, e, c, d) = c ((CLOSURE (e, x, t)) :: s, e, d) | run_t (APP (t0, t1), s, e, c, d) = run_t (t1, s, e, fn (s, e, d) => run_t (t0, s, e, fn (s, e, d) => run_a (s, e, c, d), d), d)

Ohne dump-Fortsetzung

fun eval (LIT n, s, e, c) = c ((INT n) :: s, e) | eval (VAR x, s, e, c) = c ((Env.lookup (x, e)) :: s, e) | eval (LAM (x, t), s, e, c) = c ((CLOSURE (e, x, t)) :: s, e)

| eval (APP (t0, t1), s, e, c) = eval (t1, s, e, fn (s, e) => eval (t0, s, e, fn (s, e) => apply (s, e, c)))

25


run_a (SUCC :: (INT n) :: s, e, c, d) = c ((INT (n+1)) :: s, e, d) | run_a ((CLOSURE (e’, x, t)) :: v’ :: s, e, c, d) = run_t (t, nil, Env.extend (x, v’, e’), fn (s, _, d) => d s, fn (v :: nil) => c (v :: s, e, d))

Proposition 3: Die Quellenprogrammen sie das gleiche Resultat

apply (SUCC :: (INT n) :: s, e, c) = c ((INT (n+1)) :: s, e) | apply ((CLOSURE (e’, x, t)) :: v’ :: s, e, c) = let val (v :: nil) = eval (t, nil, Env.extend (x, v’, e’), fn (s, _) => s)

in c (v :: s, e)

end

evaluate2 und evaluate3 erbringen

26

2.5 Ohne Control-Fortsetzung(1)

Elimination der Control-Fortsetzungsfunktion (* eval : Source.term * S * E -> S * E *) (* apply : S * E -> S * E *) (* where S = value list *) (* E = value Env.env *)

27

Vergleichen von ohne dump-fortsetzung und ohne control-Fortsetzung



(* evaluate3 : Source.program -> value *) fun evaluate3 t = let val (v :: nil) = eval (t, nil, e_init, fn (s, _ ) => s) in v end

Ohne control-Fortsetzung

(* eval : Source.term * S * E -> S * E *)(* apply : S * E -> S * E *)(* where S = value list *)(* E = value Env.env *)

(* evaluate4 : Source.program -> value *) fun evaluate4 t = let val (v :: nil, _) = eval (t, nil, e_init) in v end

28

Vergleichen von ohne dump-Fortsetzung und ohne control-Fortsetzung

Ohne dump-Fortsetzung

fun eval (LIT n, s, e, c) = c ((INT n) :: s, e) | eval (VAR x, s, e, c) = c ((Env.lookup (x, e)) :: s, e) | eval (LAM (x, t), s, e, c) = c ((CLOSURE (e, x, t)) :: s, e)

| eval (APP (t0, t1), s, e, c) = eval (t1, s, e, fn (s, e) => eval (t0, s, e, fn (s, e) => apply (s, e, c)))


fun eval (LIT n, s, e) = ((INT n) :: s, e)

| eval (VAR x, s, e) = ((Env.lookup (x, e)) :: s, e) | eval (LAM (x, t), s, e) = ((CLOSURE (e, x, t)) :: s, e)

| eval (APP (t0, t1), s, e) = let val (s, e) = eval (t1, s, e) val (s, e) = eval (t0, s, e) in apply (s, e) end

29

Vergleichen von ohne dump-Fortsetzung und ohne control-Fortsetzung

apply (SUCC :: (INT n) :: s, e, c) = c ((INT (n+1)) :: s, e) | apply ((CLOSURE (e’, x, t)) :: v’ :: s, e, c) = let val (v :: nil) = eval (t, nil, Env.extend (x, v’, e’), fn (s, _) => s)

in c (v :: s, e)

end

Proposition 4 : Die Quellenprogrammen

gleiche Resultat.

apply (SUCC :: (INT n) :: s, e) = ((INT (n+1)) :: s, e)

| apply ((CLOSURE (e’, x, t)) :: v’ :: s, e) = let val (v :: nil, _) = eval (t, nil, Env.extend (x, v’, e’)) in (v :: s, e) end

evaluate3 und evaluate4 erbringen sie das

30

2.6 Ohne-Stack Im Abschnitt 2.5 arbeiten eval und apply mit einem Stack von

Zwischenresultaten. Im folgenden wird eine Version ohne Stack definiert,

(* eval : Source.term * E -> value * E *) (* apply : value * value * E -> value * E *) (* where E = value Env.env *)

31

Vergleichen von ohne control-Fortsetzung und ohne stack


(* eval : Source.term * S * E -> S * E *)(* apply : S * E -> S * E *)(* where S = value list *)(* E = value Env.env *)

(* evaluate4 : Source.program -> value *) fun evaluate4 t = let val (v :: nil, _) = eval (t, nil, e_init) in v end

Ohne stack

(* eval : Source.term * E -> value * E *)(* apply : value * value * E -> value * E *)(* where E = value Env.env *)

(* evaluate5 : Source.program -> value *) fun evaluate5 t = let val (v’, _) = eval (t, e_init) in v’ end

32

Vergleichen von ohne control-Fortsetzung und ohne stack Ohne control-Fortsetzung

fun eval (LIT n, s, e) = ((INT n) :: s, e)

| eval (VAR x, s, e) = ((Env.lookup (x, e)) :: s, e) | eval (LAM (x, t), s, e) = ((CLOSURE (e, x, t)) :: s, e)

| eval (APP (t0, t1), s, e) = let val (s, e) = eval (t1, s, e) val (s, e) = eval (t0, s, e) in apply (s, e) end

Ohne stack

fun eval (LIT n, e) = (INT n, e)

| eval (VAR x, e) = (Env.lookup (x, e), e)

| eval (LAM (x, t), e) = (CLOSURE (e, x, t), e)

| eval (APP (t0, t1), e) = let val (v1, e) = eval (t1, e) val (v0, e) = eval (t0, e) in apply (v0, v1, e) end

33

Vergleichen von ohne control-Fortsetzung und ohne stack

apply (SUCC :: (INT n) :: s, e) = ((INT (n+1)) :: s, e)

| apply ((CLOSURE (e’, x, t)) :: v’ :: s, e) = let val (v :: nil, _) = eval (t, nil, Env.extend (x, v’, e’)) in (v :: s, e) end

Proposition 5: Die Quellenprogrammen Resultat.

apply (SUCC, INT n, e) = (INT (n+1), e) | apply (CLOSURE (e’, x, t), v’, e) = let val (v, _) = eval (t, Env.extend (x, v’, e’)) in (v, e) end

evaluate4 und evaluate5 erbringen Sie das gleiche

34

Fazit Spezifikation

run_c : S * E * c * d -> valuerun_d : S * D -> valuerun_t : term * S * E * C * D -> valuerun_a : S * E * C * D -> value

35

Fazit Spezifikation

Eliminieren die zwei Applikationsfunktion

Höhere Ordnung


run_t : term * S * E * C * D -> valuerun_a : S * E * C * D -> valuewhere C = S * E * D -> value D = S -> value

36

Fazit Spezifikation


Höhere Ordnung

Eliminieren die Dump-Fortsetzung




run_t : term * S * E * C -> stackrun_a : S * E * C -> Swhere C = S * E -> S

37

Fazit Spezifikation


Höhere Ordnung



Eliminieren die Control-Fortsetzung

Ohne Control-Fortsetzung




run_t : S * E -> S * Erun_a : S * E -> S * E

38

Fazit Spezifikation


Höhere Ordnung



Eliminieren die Control-Fortsetzung

Ohne Control-Fortsetzung Eliminieren das Stack

Ohne Stack




run_t : S * E -> S * Erun_a : S * E -> S * E

run_t : term * E -> value * Erun_a : value * value * E -> value * E

39

Ziel Das Enderesultat der Deconstruction von SECD Machine zeigt, daß

der denotationale Inhalt der Auswertungsfunktion von SECD-Maschine ist mit der Tpy:

term -> E -> value * E

term ist Typ von term E ist Typ von Umgebung value ist Typ von value

Date post:	06-Apr-2016
Category:	Documents
Upload:	nadja-hochberg
View:	215 times
Download:	0 times

1 Eine rationale Dekonstruktion von Landin’s SECD-Maschine Betreuerin: Prof. Dr. Rita Loogen...

Documents