forked from deinprogramm/schreibe-dein-programm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
i1secd.tex
2432 lines (2316 loc) · 87.8 KB
/
i1secd.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% Diese Datei ist Teil des Buchs "Schreibe Dein Programm!"
% Das Buch ist lizensiert unter der Creative-Commons-Lizenz
% "Namensnennung - Weitergabe unter gleichen Bedingungen 4.0 International (CC BY-SA 4.0)"
% https://creativecommons.org/licenses/by-sa/4.0/deed.de
\chapter{Die SECD-Maschine}\label{cha:secd}
Der $\lambda$-Kalkül ist als theoretisches Modell für berechenbare
Funktionen lange vor der Erfindung des Computers entwickelt worden.
Die Reduktionsregeln dienen dabei der Entwicklung von Beweisen über
die Äquivalenz von $\lambda$-Termen. Damit der $\lambda$-Kalkül auch
als Modell für die tatsächliche Ausführung von Programmen, auf dem
Computer geeignet ist, fehlen noch zwei Zutaten: die direkte
Definition von "<eingebauten"> Werten und Operationen wie Zahlen und
booleschen Werten sowie ein formales Auswertungsmodell. Dieses
Kapitel stellt zunächst den \textit{angewandten $\lambda$-Kalkül} vor,
der den normalen $\lambda$-Kalkül um primitive Werte und Operationen
erweitert, und dann die \textit{SECD-Maschine}, ein klassisches
Auswertungsmodell für die Call-by-Value-Reduktion. Angenehmerweise
lässt sich die SECD-Maschine auch als Programm implementieren,
was ebenfalls in diesem Kapitel geschieht. Die SECD-Maschine
kennt keine Zuweisungen; es folgt darum noch die Darstellung der
\textit{SECDH-Maschine}, die auch einen \textit{Speicher} kennt und
damit Zuweisungen korrekt modelliert.
Ab diesem Kapitel wird die Sprachebene \texttt{Schreibe
Dein Programm! - fortgeschritten} benötigt.
\section{Der angewandte $\lambda$-Kalkül}
Abschnitt~\ref{sec:lambdaprog} zeigte bereits, dass sich auch boolesche
Werte und Zahlen im $\lambda$-Kalkül durch $\lambda$-Terme darstellen
lassen. Das ist zwar aus theoretischer Sicht gut zu wissen, auf Dauer
aber etwas mühsam: Darum ist es sinnvoll, mit einer erweiterten
Version des $\lambda$-Kalküls zu arbeiten, die solche "<primitiven">
Werte direkt kennt. Abschnitt~\ref{sec:lambdaprog} hat gezeigt,
dass eine solche Erweiterung nur syntaktischer Zucker ist,
also die Ausdruckskraft des Kalküls nicht wirklich erhöht. Alle
Erkenntnisse aus dem normalen $\lambda$-Kalkül bleiben also erhalten.
Ein solcher erweiterter $\lambda$-Kalkül heißt auch
\textit{angewandter $\lambda$-Kalkül}:
\begin{definition}[Sprache des angewandten $\lambda$-Kalküls
$\mathcal{L}_{\lambda{}A}$]\index{angewandter $\lambda$-Kalkül}\label{def:lambda-angewandt}
Sei $V$ eine abzählbare Menge von Variablen. Sei $B$ eine Menge von
\textit{Basiswerten\index{Basiswert}}. Sei für eine natürliche
Zahl $n$ und $i \in \{1, \ldots, n\}$ jeweils $\Sigma^i$ eine Menge
von \textit{$i$-stelligen Primitiva\index{Primitivum}}~-- die Namen
von "<eingebauten Operationen">. Jedem $F^i\in\Sigma^i$ ist eine
$i$-stellige Funktion $F_B^i: B\times\ldots\times B \rightarrow
B$~-- ihre \textit{Operation}~--
zugordnet. Die Sprache des angewandten $\lambda$"=Kalküls, die
Menge der \textit{angewandten $\lambda$-Terme},
$\mathcal{L}_{\lambda{}A}$\index{L@$\mathcal{L}_{\lambda{}A}$}, ist
durch folgende Grammatik definiert:
\begin{grammar}
\meta{$\mathcal{L}_{\lambda{}A}$} \: \meta{$V$}
\> \| (\meta{$\mathcal{L}_{\lambda{}A}$} \meta{$\mathcal{L}_{\lambda{}A}$})
\> \| ($\lambda$\meta{$V$}.\meta{$\mathcal{L}_{\lambda{}A}$})
\> \| \meta{$B$}
\> \| (\meta{$\Sigma^1$}~\meta{$\mathcal{L}_{\lambda{}A}$})
\> \| (\meta{$\Sigma^2$}~\meta{$\mathcal{L}_{\lambda{}A}$}~\meta{$\mathcal{L}_{\lambda{}A}$})
\> \ldots
\> \| (\meta{$\Sigma^n$}~\meta{$\mathcal{L}_{\lambda{}A}$}~\ldots~\meta{$\mathcal{L}_{\lambda{}A}$}) \quad \textrm{($n$-mal)}
\end{grammar}
Die Grammatik ist abgekürzt notiert: Die letzen Klauseln besagen,
dass es für jede Stelligkeit $i$ eine Klausel mit \meta{$\Sigma^i$} gibt,
bei der jeweils $i$ Wiederholungen von
\meta{$\mathcal{L}_{\lambda{}A}$}~-- entsprechend der Stelligkeit
der Primitiva in $\Sigma^i$.
%
Dabei heißen Terme der Form $(F^k~e_1~\ldots~e_k)$ auch
\textit{primitive Applikationen\index{primitive Applikation}}.
\end{definition}
%
In diesem Kapitel dienen normalerweise die Zahlen als Basiswerte mit
den üblichen Operationen wie $+$, $-$, $\ast$, $/$ etc. Damit sind
Terme wie zum Beispiel $(+~(-~5~3)~17)$ möglich.
Im angewandten $\lambda$-Kalkül kommen zu den Werten aus
Definition~\ref{def:wert} die Basiswerte dazu:
%
\begin{definition}[Werte im angewandten $\lambda$-Kalkül]\label{def:wert-angewandt}
Im angewandten $\lambda$-Kalkül heißen die Abstraktionen und
Basiswerte kollektiv \textit{Werte}. Ein $\lambda$-Term, der kein
Wert\index{Wert} ist, heißt \textit{Nichtwert\index{Nichtwert}}.
\end{definition}
Damit die primitiven Operationen auch tatsächlich eine Bedeutung
bekommen, muss eine spezielle Reduktionsregel für sie eingeführt
werden:
%
\begin{definition}[$\delta$-Reduktion]\index{delta-Reduktion@$\delta$-Reduktion}
\begin{displaymath}
(F^k~e_1~\ldots~e_k) \rightarrow_{\delta} F_B^k(e_1, \ldots, e_k)
\quad e_1, \ldots, e_k \in B
\end{displaymath}
\end{definition}
%
Diese Regel besagt, dass eine primitive Applikation, wenn alle
Operanden Werte sind, durch Anwendung der entsprechenden Operation
reduziert werden kann. Damit wird z.B.\ der
obige Beispielterm folgendermaßen reduziert:
%
\begin{displaymath}
(+~(-~5~3)~17) \rightarrow_{\delta} (+~2~17) \rightarrow_{\delta} 19
\end{displaymath}
\section{Die einfache SECD-Maschine}
Wie schon in Abschnitt~\ref{sec:scheme-auswertung} erwähnt, ist
der Call-by-Value-$\lambda$-Kalkül\index{Call-by-Value-Reduktion}
ein Modell für die Auswertung der Lehrsprachen und viele andere
Programmiersprachen .
Allerdings ist Definition~\ref{def:call-by-value} strenggenommen etwas
vage: Es wird immer nur der Subterm reduziert, der
"<möglichst weit links innen steht">, aber was das heißt, ist nicht
genau definiert. Außerdem ist Reduktion zwar ein
mächtiges formales Modell, entspricht aber nicht der
Ausführungsmethode tatsächlicher Programmiersprachen auf echten
Prozessoren. Ein präzises und echten Maschinen deutlich näheres
Modell ist die \textit{SECD-Maschine\index{SECD-Maschine}}, erfunden
schon in den 60er Jahren von Peter Landin~\cite{Landin1964}, und
seitdem die Grundlage für zahllose Implementierungen von
Call-by-Value-Sprachen. (Die Darstellung hier ist gegenüber Landins
ursprünglicher Formulierung etwas modernisiert.)
Damit ein Programm aus dem angewandten $\lambda$-Kalkül mit der
SECD-Maschine ausgewertet werden kann, muss es erst einmal in einen
speziellen \textit{Maschinencode\index{Maschinencode}} übersetzt oder
"<compiliert"> werden. Der Maschinencode besteht, anders als der
$\lambda$-Kalkül, nicht aus geschachtelten Termen, sondern aus einer
Folge von \textit{Instruktionen\index{Instruktion}}.
\begin{definition}[Maschinencode]\label{def:secd-code}
In der folgenden Definition ist $I$ die Menge der Instruktionen:
\begin{grammar}
\meta{I} \: \meta{B}
\> \| \meta{V}
\> \| ap
\> \| prim$_{F^i}$ \textrm{für alle $F^i \in \Sigma^i$}
\> \| (\meta{V}, \meta{C})
\end{grammar}
%
Ein Maschinencode-Programm ist eine Folge von Instruktionen:
%
\begin{displaymath}
C = I^\ast
\end{displaymath}
\end{definition}
Ein Term aus dem angewandten $\lambda$-Kalkül wird mit Hilfe folgender
Funktion in Maschinencode übersetzt:
%
\begin{eqnarray*}
\llbracket \underline{~} \rrbracket &:& \mathcal{L}_{\lambda{}A}
\rightarrow C\\
\llbracket e \rrbracket &\deq&
\begin{cases}
b & \textrm{falls $e = b \in B$}\\
v & \textrm{falls $e = v \in V$}\\
\llbracket e_0\rrbracket~\llbracket e_1\rrbracket~\mathtt{ap}
& \textrm{falls $e = (e_0~e_1)$}\\
\llbracket e_1\rrbracket~\ldots~\llbracket e_k\rrbracket~\mathtt{prim}_{F^k}
& \textrm{falls $e = (F~e_1~\ldots~e_k)$}\\
(v, \llbracket e_0\rrbracket) & \textrm{falls $e = \lambda v.e_0$}
\end{cases}
\end{eqnarray*}
%
Die Übersetzungsfunktion "<linearisiert"> einen $\lambda$-Term. Zum
Beispiel bedeutet die Übersetzung $\llbracket e_0\rrbracket~\llbracket
e_1\rrbracket~\mathtt{ap}$ für einen Term $(e_0~e_1)$, dass zuerst
$e_0$ ausgewertet wird, danach wird $e_1$ ausgewertet, und schließlich wird die
eigentliche Applikation ausgeführt: Entsprechend steht $\mathtt{ap}$
für "<Applikation ausführen"> und $\mathtt{prim}_{F^k}$ für "<Primitiv
$F$ ausführen">. Basiswerte und Variablen werden im Maschinencode
belassen. Ein $\lambda$-Term wird übersetzt in ein Tupel aus seiner
Variable und dem Maschinencode für seinen Rumpf.
Durch die Linearisierung sind die Instruktionen schon in einer Liste in der
Reihenfolge ihrer Ausführung aufgereiht. Insbesondere hat die
Linearisierung den Begriff "<links innen"> formalisiert: der jeweils
am weitesten links innen stehende Redex steht in der Liste der
Instruktionen vorn.
Beispiel:
%
\begin{eqnarray*}
\llbracket \lambda f.\lambda x.\lambda y.f~(+~x~(*~y~2))\rrbracket
&=&
(f, \llbracket \lambda x.\lambda y.f~(+~x~(*~y~2))\rrbracket)\\
&=&
(f, (x, \llbracket \lambda y.f~(+~x~(*~y 2))\rrbracket))\\
&=&
(f, (x, (y, \llbracket f~(+~x~(*~y 2))\rrbracket)))\\
&=&
(f, (x, (y, \llbracket f\rrbracket \llbracket (+~x~(*~y
2))\rrbracket \mathtt{ap})))\\
&=&
(f, (x, (y, f \llbracket (+~x~(*~y 2))\rrbracket\mathtt{ap})))\\
&=&
(f, (x, (y, f \llbracket x\rrbracket \llbracket (*~y~2)\rrbracket \mathtt{prim}_+~\mathtt{ap})))\\
&=&
(f, (x, (y, f~x \llbracket (*~y~2)\rrbracket \mathtt{prim}_+~\mathtt{ap})))\\
&=&
(f, (x, (y, f~x \llbracket y\rrbracket \llbracket 2\rrbracket \mathtt{prim}_*~\mathtt{prim}_+~\mathtt{ap})))\\
&=&
(f, (x, (y, f~x~y \llbracket 2\rrbracket \mathtt{prim}_*~\mathtt{prim}_+~\mathtt{ap})))\\
&=&
(f, (x, (y, f~x~y~2~\mathtt{prim}_*~\mathtt{prim}_+~\mathtt{ap})))\\
\end{eqnarray*}
%
Das Beispiel zeigt deutlich, wie der Rumpf der innersten Abstraktion
in eine lineare Folge von Instruktionen übersetzt wird, die genau der
Call-by-Value-Reduktionsstrategie entspricht: erst $f$ auswerten, dann
$x$, dann $y$, dann das Primitiv $*$ anwenden, dann $+$, und
schließlich die Applikation durchführen.
Nun zur eigentlichen SECD-Maschine~-- sie funktioniert ähnlich wie ein
Reduktionskalkül, operiert aber auf sogenannten
\textit{Maschinenzuständen}: die Maschine überführt also einen
Maschinenzustand durch einen Auswertungsschritt in einen neuen
Maschinenzustand. Ein Maschinenzustand ist dabei ein 4-Tupel aus der
Menge $S\times E\times C\times D$ (daher der Name der Maschine). Die
Buchstaben sind deshalb so gewählt, weil $S$ der sogenannte
\textit{Stack\index{Stack}}, $E$ die sogenannte
\textit{Umgebung\index{Umgebung}} beziehungsweise auf englisch das
\textit{Environment\index{Environment}}, $C$ der schon bekannte
Maschinencode beziehungsweise \textit{Code\index{Code}} und $D$ der
sogenannte \textit{Dump\index{Dump}} ist. Die formalen Definitionen
dieser Mengen sind wie folgt; dabei ist $W$ die Menge der Werte:
%
\begin{eqnarray*}
S &=& W^\ast\\
E &=& \mathcal{P}(V\times W)\\
D &=& (S\times E \times C)^\ast\\
W &=& B \cup (V\times C\times E)
\end{eqnarray*}
%
Der Stack ist dabei eine Folge von Werten. In der Maschine sind dies
die Werte der zuletzt ausgewerteten Terme, wobei der zuletzt
ausgewertete Term vorn beziehungsweise "<oben"> steht. Die Umgebung ist eine
partielle Abbildung von Variablen auf Werte: sie ersetzt die
Substitution in der Reduktionsrelation des $\lambda$-Kalküls. Anstatt
dass Werte für Variablen eingesetzt werden, merkt sich die Umgebung
einfach, an welche Werte die Variablen gebunden sind. Erst wenn der
Wert einer Variablen benötigt wird, holt ihn die Maschine aus der
Umgebung. Der Dump schließlich ist eine Liste früherer Zustände der
Maschine: er entspricht dem Kontext\index{Kontext} im
Substitutionsmodell.
Die Menge $W$ schließlich entspricht dem Wertebegriff aus
Definition~\ref{def:wert-angewandt}: Die Basiswerte gehören dazu,
außerdem Tripel aus $(V\times C\times E)$. Ein solches Tripel,
genannt \textit{Closure\index{Closure}}~-- repräsentiert den Wert
einer Abstraktion~-- es besteht aus der Variable einer Abstraktion,
dem Maschinencode ihres Rumpfs und der Umgebung, die notwendig ist, um
die Abstraktion anzuwenden: Die Umgebung wird benötigt, damit die
freien Variablen der Abstraktion entsprechend der lexikalischen
Bindung\index{lexikalische Bindung} ausgewertet werden können. Dies
ist anders als im Substitutionsmodell, wo Variablen bei der
Applikation direkt ersetzt werden und damit verschwinden. Eine
Closure ist also einfach die Repräsentation einer Funktion.
Im Verlauf der Auswertung werden Umgebungen häufig um neue Bindungen
von einer Variable an einen Wert erweitert. Dazu ist die Notation
$e[v\mapsto w]$ nützlich. $e[v\mapsto w]$ konstruiert aus einer
Umgebung $e$ eine neue Umgebung, in der die Variable $v$ an den Wert
$w$ gebunden ist. Hier ist die Definition:
%
\begin{displaymath}
e[v\mapsto w] \deq (e \setminus \{ (v, w') | (v, w') \in e \}) \cup \{
(v, w) \}
\end{displaymath}
%
Es wird also zunächst eine eventuell vorhandene alte Bindung entfernt
und dann eine neue hinzugefügt.
Um einen $\lambda$-Term $e$ in die SECD-Maschine zu "<injizieren">,
wird er in einen Anfangszustand $(\epsilon, \varnothing, \llbracket
e\rrbracket, \epsilon)$ übersetzt. Dann wird dieser Zustand
wiederholt in die Zustandsübergangsrelation $\hookrightarrow$
gefüttert. In der folgenden Definition von $\hookrightarrow$ sind
Bezeichner mit einem Unterstrich versehen, wenn es sich um Folgen
handelt, also z.B.\ \underline{s} für einen Stack:
%
\begin{eqnarray}
\hookrightarrow &\in& \mathcal{P}((S\times E\times C\times D) \times (S\times E\times C\times D))\notag\\
(\underline{s}, e, b\underline{c}, \underline{d})
&\hookrightarrow&
(b\underline{s}, e, \underline{c}, \underline{d})
\label{secd:base}
\\
(\underline{s}, e, v\underline{c}, \underline{d})
&\hookrightarrow&
(e(v)\underline{s}, e, \underline{c}, \underline{d})
\label{secd:variable}
\\
(b_k\ldots b_1 \underline{s}, e, \mathtt{prim}_{F^k}\underline{c}, \underline{d})
&\hookrightarrow&
(b\underline{s}, e, \underline{c}, \underline{d})
\label{secd:prim}
\\ && \textrm{wobei $F^k\in\Sigma^k$ und $F^k_B(b_1,\ldots,b_k) = b$}\notag
\\
(\underline{s}, e, (v, \underline{c'}) \underline{c}, \underline{d})
&\hookrightarrow&
((v, \underline{c'}, e) \underline{s}, e, \underline{c}, \underline{d})
\label{secd:abstraction}
\\
(w (v,\underline{c'}, e') \underline{s}, e, \mathtt{ap}~\underline{c}, \underline{d})
&\hookrightarrow&
(\epsilon, e'[v\mapsto w], \underline{c'}, (\underline{s}, e, \underline{c}) \underline{d})
\label{secd:app}
\\
(w, e, \epsilon, (\underline{s'}, e', \underline{c'}) \underline{d})
&\hookrightarrow&
(w\underline{s'}, e', \underline{c'}, \underline{d})
\label{secd:return}
\end{eqnarray}
%
Die Regeln definieren eine Fallunterscheidung nach der ersten
Instruktion der Code"=Komponente des Zustands, beziehungsweise greift die letzte
Regel, wenn der Code leer ist. Der Reihe nach arbeiten die Regeln wie
folgt:
%
\begin{itemize}
\item Regel~\ref{secd:base} (die
\textit{Literalregel\index{Literalregel}}) schiebt einen Basiswert
direkt auf den Stack.
\item Regel~\ref{secd:variable} (die
\textit{Variablenregel\index{Variablenregel}}) ermittelt den Wert
einer Variable aus der Umgebung und schiebt diesen auf den Stack.
\item Regel~\ref{secd:prim} ist die
\textit{Primitivregel\index{Primitivregel}}. Bei einer primitiven
Applikation müssen soviele Basiswerte oben auf dem Stack liegen wie
die Stelligkeit des Primitivs. Dann ermittelt die Primitivregel das Ergebnis der
primitiven Applikation und schiebt es oben auf den Stack.
\item Regel~\ref{secd:abstraction} ist die
\textit{Abstraktionsregel\index{Abstraktionsregel}}: Das Tupel
$(v,\underline{c'})$ ist bei der Übersetzung aus einer Abstraktion
entstanden. Die Regel ergänzt $v$ und $\underline{c'}$ mit
$e$ zu einer Closure, die auf den Stack geschoben wird.
\item Regel~\ref{secd:app} ist die
\textit{Applikationsregel\index{Applikationsregel}}: Bei einer
Applikation müssen oben auf dem Stack ein Wert sowie eine Closure
liegen. (Zur Erinnerung: Eine Applikation kann nur ausgewertet
werden, wenn eine Abstraktion vorliegt. Abstraktionen werden zu
Closures ausgewertet.) In einem solchen Fall "<sichert"> die
Applikation den aktuellen Zustand auf den Dump, und die Auswertung fährt mit
einem leeren Stack, der Umgebung aus der Closure~-- erweitert um
eine Bindung für die Variable~-- und dem Code aus der Closure fort.
\item Regel~\ref{secd:return} ist die
\textit{Rückkehrregel\index{Rückkehrregel}}: Sie ist anwendbar,
wenn das Ende des Codes erreicht ist. Das heißt, dass gerade
die Auswertung einer Applikation fertig ist. Auf dem Dump liegt
aber noch ein gesicherter Zustand, der jetzt "<zurückgeholt"> wird.
\end{itemize}
%
Hier ein Beispiel für den Ablauf der SECD-Maschine für den Term
$(((\lambda x.\lambda y.(+~x~y))~1)~2)$:
% (secd-step*/tex (inject-secd '(((lambda (x) (lambda (y) (+ x y))) 1) 2)))
%
\begin{displaymath}
\begin{array}{l@{}llll}
&(\epsilon, &\varnothing, &(x, (y, x~y~\mathtt{prim}_+))~1~\mathtt{ap}~2~\mathtt{ap}, &\epsilon)\\
\hookrightarrow{}&((x, (y, x~y~\mathtt{prim}_+), \varnothing), &\varnothing, &1~\mathtt{ap}~2~\mathtt{ap}, &\epsilon)\\
\hookrightarrow{}&(1~(x, (y, x~y~\mathtt{prim}_+), \varnothing), &\varnothing, &\mathtt{ap}~2~\mathtt{ap}, &\epsilon)\\
\hookrightarrow{}&(\epsilon, &\{(x, 1)\}, &(y, x~y~\mathtt{prim}_+), &(\epsilon, \varnothing, 2~\mathtt{ap}))\\
\hookrightarrow{}&((y, x~y~\mathtt{prim}_+, \{(x, 1)\}), &\{(x, 1)\}, &\epsilon, &(\epsilon, \varnothing, 2~\mathtt{ap}))\\
\hookrightarrow{}&((y, x~y~\mathtt{prim}_+, \{(x, 1)\}), &\varnothing, &2~\mathtt{ap}, &\epsilon)\\
\hookrightarrow{}&(2~(y, x~y~\mathtt{prim}_+, \{(x, 1)\}), &\varnothing, &\mathtt{ap}, &\epsilon)\\
\hookrightarrow{}&(\epsilon, &\{(x, 1), (y, 2)\}, &x~y~\mathtt{prim}_+, &(\epsilon, \varnothing, \epsilon))\\
\hookrightarrow{}&(1, &\{(x, 1), (y, 2)\}, &y~\mathtt{prim}_+, &(\epsilon, \varnothing, \epsilon))\\
\hookrightarrow{}&(2~1, &\{(x, 1), (y, 2)\}, &\mathtt{prim}_+, &(\epsilon, \varnothing, \epsilon))\\
\hookrightarrow{}&(3, &\{(x, 1), (y, 2)\}, &\epsilon, &(\epsilon, \varnothing, \epsilon))\\
\hookrightarrow{}&(3, &\varnothing, &\epsilon, &\epsilon)
\end{array}
\end{displaymath}
%
Die Zustandsübergangsrelation $\hookrightarrow$ ist nun die Grundlage
für die \textit{Auswertungsfunktion\index{Auswertungsfunktion}} der
SECD-Maschine, die für einen $\lambda$-Term dessen Bedeutung
ausrechnet. Dies ist scheinbar ganz einfach:
%
\begin{eqnarray*}
\mathit{eval}_\mathit{SECD} & : & \mathcal{L}_{\lambda{}A} \rightarrow B\\
\mathit{eval}_\mathit{SECD}(e) &= & x \textrm{ wenn } (\epsilon, \varnothing, \llbracket e\rrbracket, \epsilon)
\hookrightarrow^* (x, e, \epsilon, \epsilon)
\end{eqnarray*}
%
Diese Definition hat jedoch zwei Haken:
%
\begin{itemize}
\item Die Auswertung von $\lambda$-Termen terminiert nicht immer (wie
zum Beispiel für den "<Endlos"=Term"> $(\lambda x.(x~x))~(\lambda x.(x~x))$), es kommt
also nicht immer dazu, dass die Zustandsübergangsrelation bei einem
Zustand der Form $(\epsilon, \varnothing, \llbracket e\rrbracket,
\epsilon)$ terminiert.
\item Das $x$ aus dieser Definition ist nicht immer ein Basiswert~--
es kann auch eine Closure sein.
\end{itemize}
%
Der erste Haken sorgt dafür, dass die Auswertungsfunktion nur eine
Relation im Sinne einer "<partiellen Funktion"> ist. Meist wird
trotzdem von einer Auswertungsfunktion gesprochen. Beim zweiten
Haken, wenn $x$ eine Closure ist, lässt sich mit dem Resultat nicht
viel anfangen: Um die genaue Bedeutung der Closure herauszubekommen,
müsste sie angewendet werden~-- das Programm ist aber schon fertig
gelaufen. Es ist also gar nicht sinnvoll, zwischen verschiedenen
Closures zu unterscheiden. Darum wird für die Zwecke der
Auswertungsfunktion eine Menge $Z$ der \textit{Antworten\index{Antwort}}
definiert, die einen designierten Spezialwert für Closures enthält:
%
\begin{displaymath}
Z = B \cup \{ \texttt{function} \}
\end{displaymath}
%
Damit lässt sich die Evaluationsfunktion wie folgt definieren:
%
\begin{eqnarray*}
\mathit{eval}_\mathit{SECD} & \in & \mathcal{L}_{\lambda{}A} \times Z\\
\mathit{eval}_\mathit{SECD}(e) & = &
\begin{cases}
b & \textrm{falls } (\epsilon, \varnothing, \llbracket e\rrbracket, \epsilon)
\hookrightarrow^* (b, e, \epsilon, \epsilon)\\
\texttt{function} & \textrm{falls } (\epsilon, \varnothing, \llbracket e\rrbracket, \epsilon)
\hookrightarrow^* ((v, \underline{c}, e'), e, \epsilon, \epsilon)\\
\end{cases}
\end{eqnarray*}
\section{\texttt{Quote} und Symbole}
\label{sec:quote}
Dieses Kapitel wird ab hier Gebrauch von einer weiteren
Sprachebene\index{Sprachebene!fortgeschritten} in
\drscheme{} machen, nämlich \texttt{Die Macht der Abstraktion -
fortgeschritten}. Diese Ebene muss mit dem \drscheme{}-Menü \texttt{Sprache}
unter \texttt{Sprache auswählen} aktiviert sein, damit die
Programme dieses Kapitels funktionieren.
Die entscheidende Änderung gegenüber den früheren Sprachebenen ist
die Art, mit der die REPL Werte ausdruckt. (Diese neue Schreibweise,
ermöglicht, die Programme des Interpreters, die als Werte
repräsentiert sind, korrekt auszudrucken.) Bei Zahlen, Zeichenketten
und booleschen Werten bleibt alles beim alten:
%
\begin{alltt}
5
\evalsto{} 5
"Mike ist doof"
\evalsto{} "Mike ist doof"
#t
\evalsto{} #t
\end{alltt}
%
Bei Listen sieht es allerdings anders aus:
%
\begin{alltt}
(list 1 2 3 4 5 6)
\evalsto{} (1 2 3 4 5 6)
\end{alltt}
%
Die REPL druckt also eine Liste aus, indem sie zuerst eine öffnende
Klammer ausdruckt, dann die Listenelemente (durch Leerzeichen
getrennt) und dann eine schließende Klammer.
Das funktioniert auch für die leere Liste:
%
\begin{alltt}
empty
\evalsto{} ()
\end{alltt}
%
Mit der neuen Sprachebene bekommt außerdem der Apostroph, der dem
Literal\index{Literal} für die leere Liste voransteht, eine erweiterte Bedeutung.
Unter anderem kann der Apostroph benutzt werden, um Literale für
Listen zu formulieren:
%
\begin{alltt}
'(1 2 3 4 5 6)
\evalsto{} (1 2 3 4 5 6)
'(1 #t "Mike" (2 3) "doof" 4 #f 17)
\evalsto{} (1 #t "Mike" (2 3) "doof" 4 #f 17)
'()
\evalsto{} ()
\end{alltt}
%
In der neuen Sprachebene benutzen die Literale und die ausgedruckten
externen Repräsentationen für Listen also die gleiche
Notation\index{Repräsentation}. Sie unterscheiden sich nur dadurch,
dass beim Literal der Apostroph voransteht. Der Apostroph funktioniert
auch bei Zahlen, Zeichenketten und booleschen Werten:
%
\begin{alltt}
'5
\evalsto{} 5
'"Mike ist doof"
\evalsto{} "Mike ist doof"
'#t
\evalsto{} #t
\end{alltt}
%
Der Apostroph am Anfang eines Ausdrucks
kennzeichnet diesen also als Literal. Der Wert des Literals wird
genauso ausgedruckt, wie es im Programm steht. (Abgesehen von
Leerzeichen und Zeilenumbrüchen.) Der Apostroph heißt auf englisch
"<quote">\index{quote@\texttt{quote}}, und deshalb ist diese
Literalschreibweise auch unter diesem Namen bekannt. Bei Zahlen,
Zeichenketten und booleschen Literalen ist auch ohne Quote klar, dass
es sich um Literale handelt. Das Quote ist darum bei ihnen rein
optional; sie heißen
\textit{selbstquotierend}\index{selbstquotierend}.
Bei Listen hingegen sind Mißverständnisse mit anderen
zusammengesetzten Formen möglich, die ja auch mit einer öffnenden Klammer
beginnen: \footnote{Tatsächlich ist die neue Schreibweise für externe
Repräsentationen die Standard-Repräsentation in Scheme. Die
früheren Sprachebenen benutzten die alternative Schreibweise, um die
Verwirrung zwischen Listenliteralen und zusammengesetzten Formen zu
vermeiden.}
\begin{alltt}
(1 2 3 4 5 6)
\evalsto{} procedure application: expected procedure, given: 1;
arguments were: 2 3 4 5 6
\end{alltt}
%
Mit der Einführung von Quote kommt noch eine völlig neue Sorte Werte
hinzu: die \textit{Symbole\index{Symbol}}. Symbole sind Werte ähnlich wie Zeichenketten und
bestehen aus Text. Sie unterscheiden sich allerdings dadurch, dass sie
als Literal mit Quote geschrieben und in der REPL ohne
Anführungszeichen ausgedruckt werden:
%
\begin{alltt}
'mike
\evalsto{} mike
'doof
\evalsto{} doof
\end{alltt}
%
Symbole lassen sich mit dem Prädikat
\texttt{symbol?\index{symbol@\texttt{symbol?}}} von anderen Werten
unterscheiden:
%
\begin{alltt}
(symbol? 'mike)
\evalsto{} #t
(symbol? 5)
\evalsto{} #f
(symbol? "Mike")
\evalsto{} #f
\end{alltt}
%
Vergleichen lassen sich Symbole mit \texttt{equal?} (siehe
Abbildung~\ref{scheme:equalp}):
\begin{alltt}
(equal? 'mike 'herb)
\evalsto{} #f
(equal? 'mike 'mike)
\evalsto{} #t
\end{alltt}
Symbole können nicht aus beliebigem Text bestehen.
Leerzeichen sind zum Beispiel verboten. Tatsächlich entsprechen die
Namen der zulässigen Symbole genau den Namen von Variablen:
%
\begin{alltt}
'karl-otto
\evalsto{} karl-otto
'mehrwertsteuer
\evalsto{} mehrwertsteuer
'duftmarke
\evalsto{} duftmarke
'lambda
\evalsto{} lambda
'+
\evalsto{} +
'*
\evalsto{} *
\end{alltt}
%
Diese Entsprechung wird in diesem Kapitel noch eine entscheidene Rolle
spielen. Symbole können natürlich auch in Listen und damit auch in
Listenliteralen vorkommen:
%
\begin{alltt}
'(karl-otto mehrwertsteuer duftmarke)
\evalsto{} (karl-otto mehrwertsteuer duftmarke)
\end{alltt}
%
Mit Hilfe von Symbolen können Werte konstruiert werden, die in der REPL
ausgedruckt wie Ausdrücke aussehen:
%
\begin{alltt}
'(+ 1 2)
\evalsto{} (+ 1 2)
'(lambda (n) (+ n 1))
\evalsto{} (lambda (n) (+ n 1))
\end{alltt}
%
Auch wenn diese Werte wie Ausdrücke so aussehen, sind sie doch ganz
normale Listen: der Wert von \verb|'(+ 1 2)| ist eine Liste mit drei
Elementen: das Symbol \verb|+|, die Zahl \texttt{1} und die Zahl
\texttt{2}. Der Wert von \verb|'(lambda (n) (+ n 1))| ist ebenfalls
eine Liste mit drei Elementen: das Symbol \verb|lambda|, eine Liste
mit einem einzelnen Element, nämlich dem Symbol \texttt{n}, und einer
weiteren Liste mit drei Elementen: dem Symbol \verb|+|, dem Symbol
\texttt{n} und der Zahl \texttt{1}.
Quote hat noch eine weitere verwirrende Eigenheit:
%
\begin{alltt}
''()
\evalsto{} '()
\end{alltt}
%
Dieses Literal bezeichnet nicht die leere Liste (dann würde nur
\texttt{()} ausgedruckt, ohne Quote), sondern etwas anderes:
%
\begin{alltt}
(cons? ''())
\evalsto{} #t
(first ''())
\evalsto{} quote
(rest ''())
\evalsto{} (())
\end{alltt}
%
Der Wert des Ausdrucks \verb|''()| ist also eine Liste mit zwei
Elementen: das erste Element ist das Symbol \texttt{quote} und das
zweite Element ist die leere Liste. \texttt{'$t$}
ist selbst also nur syntaktischer Zucker, und zwar für \texttt{(quote
$t$)}:
%
\begin{alltt}
(equal? (quote ()) '())
\evalsto{} #t
(equal? (quote (quote ())) ''())
\evalsto{} #t
\end{alltt}
%
Quote erlaubt die Konstruktion von Literalen für viele Werte, aber
nicht für alle. Ein Wert, für den Quote ein Literal konstruieren kann,
heißt \textit{repräsentierbarer
Wert\index{repräsentierbarer Wert}}. Die folgende induktive
Definition spezifiziert, was ein repräsentierbarer Wert ist:
%
\begin{itemize}
\item Zahlen, boolesche Werte, Zeichenketten und Symbole sind
repräsentierbare Werte.
\item Eine Liste aus repräsentierbaren Werten ist ihrerseits ein
repräsentierbarer Wert.
\item Nichts sonst ist ein repräsentierbarer Wert.
\end{itemize}
\section{Implementierung der SECD-Maschine}
Die SECD-Maschine ist ein Modell für die Implementierung des
$\lambda$-Kalküls. Eine solche Implementierung lässt sich in
einfach bauen~-- dieser Abschnitt zeigt, wie. Der grobe
Fahrplan ergibt sich dabei aus der Struktur der SECD-Maschine selbst:
Nach den obligatorischen Datendefinitionen müssen zunächst Terme in
Maschinencode übersetzt werden. Dann kommt die
Zustandsübergangsfunktion und schließlich die Auswertungsfunktion an
die Reihe.
\subsection{Datenanalyse}
\label{sec:secd-datenanalyse}
Die erste Aufgabe ist dabei zunächst, wie immer, die Datenanalyse: Am
Anfang stehen die Terme des angewandten $\lambda$-Kalküls. Eine
geeignete Repräsentation mit Listen und Symbolen lässt dabei die Terme
in der "<fortgeschrittenen"> Sprachebene genau wie entsprechenden
Programm-Terme aussehen:
\noindent\begin{tabular}{lll}
\texttt{(+ 1 2)} & steht für & $(+~1~2)$\\
\texttt{(lambda (x) x)} & steht für & $\lambda x.x$\\
\texttt{((lambda (x) (x x)) (lambda (x) (x x)))} & steht für &
$(\lambda x.(x~x))~(\lambda x.(x~x))$\\
etc.
\end{tabular}
Die Datendefinition dafür orientiert sich direkt an
Definition~\ref{def:lambda-angewandt}:
%
\begin{verbatim}
Ein Lambda-Term ist eins der folgenden:
; - ein Symbol (für eine Variable)
; - eine zweielementige Liste (für eine reguläre Applikation)
; - eine Liste der Form (lambda (x) e) (für eine Abstraktion)
; - ein Basiswert
; - eine Liste mit einem Primitiv als erstem Element
; (für eine primitive Applikation)
\end{verbatim}
%
Hier die dazu passende Signatur-Definition:
%
\begin{verbatim}
(define term
(signature
(mixed symbol
application
abstraction
base
primitive-application)))
\end{verbatim}
%
Die Signaturen für \texttt{application} etc.\ müssen noch definiert
werden.
Um Verzweigungen über die Sorte \texttt{term} zu ermöglichen, müssen
Prädikate für die einzelnen Teilsorten geschrieben werden. Diese
können dann für die Definition der entsprechenden Signaturen benutzt
werden.
%
\begin{verbatim}
(: application? (%a -> boolean))
(define application?
(lambda (t)
(and (cons? t)
(not (equal? 'lambda (first t)))
(not (primitive? (first t))))))
(define application (signature (predicate application?)))
; Prädikat für Abstraktionen
(: abstraction? (%a -> boolean))
(define abstraction?
(lambda (t)
(and (cons? t)
(equal? 'lambda (first t)))))
(define abstraction (signature (predicate abstraction?)))
; Prädikat für primitive Applikationen
(: primitive-application? (%a -> boolean))
(define primitive-application?
(lambda (t)
(and (cons? t)
(primitive? (first t)))))
(define primitive-application (signature (predicate primitive-application?)))
\end{verbatim}
%
Die Definition lässt noch offen, was genau ein "<Basiswert"> und was ein
"<Primitiv"> ist. Auch hierfür werden noch Datendefinitionen
benötigt, zuerst für Basiswerte. Der Einfachheit halber beschränkt
sich die Implementierung erst einmal auf boolesche Werte und Zahlen:
%
\begin{verbatim}
; Ein Basiswert ist ein boolescher Wert oder eine Zahl
\end{verbatim}
%
Damit Basiswerte in Fallunterscheidungen von den anderen Arten von
Termen unterschieden werden können, wird ein Prädikat benötigt:
%
\begin{verbatim}
; Prädikat für Basiswerte
(: base? (%a -> boolean))
(define base?
(lambda (v)
(or (boolean? v) (number? v))))
(define base (signature (predicate base?)))
\end{verbatim}
%
Als Nächstes sind Primitive gefragt: Am obigen Beispiel ist zu
erkennen, dass z.B.\ \texttt{+} ein Primitiv sein sollte. Die
Datendefinition für eine kleine beispielhafte Menge von Primitiven ist
wie folgt:
%
\begin{verbatim}
; Ein Primitiv ist eins der Symbole +, -, *, /, =
\end{verbatim}
%
Da die Primitive genau wie die Variablen Symbole sind, stehen die
Primitive als Variablen nicht mehr zur Verfügung: Alle Symbole, die
keine Primitive sind, sind also Variablen. Das dazugehörige Prädikat
ist das folgende:
%
\begin{verbatim}
; Prädikat für Primitive
(: primitive? (%a -> boolean))
(define primitive?
(lambda (s)
(or (equal? '+ s)
(equal? '- s)
(equal? '* s)
(equal? '/ s)
(equal? '= s))))
(define primitive (signature (predicate primitive?)))
\end{verbatim}
%
Bevor nun ein die SECD-Maschine einen Term verarbeiten kann, muss
dieser erst in Maschinencode übersetzt werden. Dabei entsteht aus
Definition~\ref{def:secd-code} direkt Daten- und Signatur-Definitionen
für Instruktionen und Maschinencode:
%
\begin{verbatim}
; Eine Instruktion ist eins der folgenden:
; - ein Basiswert
; - eine Variable
; - eine Applikations-Instruktion
; - eine Instruktion für eine primitive Applikation
; - eine Abstraktion
(define instruction
(signature
(mixed base
symbol
ap
tailap
prim
abs))
; Eine Maschinencode-Programm ist eine Liste von Instruktionen.
(define machine-code (signature (list-of instruction)))
\end{verbatim}
%
Bei der Definition von Instruktionen ist wieder einiges Wunschdenken
im Spiel. Basiswerte und Variablen sind wie bei den Termen. Die
restlichen Fälle werden durch eigene Datendefinitionen abgebildet.
Wie schon bei den leeren Bäumen sind Record-Definitionen ohne Felder
im Spiel, die Fallunterscheidungen möglich machen:
%
\begin{verbatim}
; Eine Applikations-Instruktion ist ein Wert
; (make-ap)
(define-record-procedures ap
make-ap ap?
())
(: make-ap (-> ap))
; Die Instruktion für eine primitive Applikation
; ist ein Wert
; (real-make-prim op arity)
; wobei op ein Symbol und arity die Stelligkeit
; ist
(define-record-procedures prim
real-make-prim prim?
(prim-operator prim-arity))
(: make-prim (symbol natural -> prim))
; Eine Abstraktions-Instruktion ist ein Wert
; (make-abs v c)
; wobei v ein Symbol (für eine Variable) und c
; Maschinencode ist
(define-record-procedures abs
make-abs abs?
(abs-variable abs-code))
(: make-abs (symbol machine-code -> abs))
\end{verbatim}
%
Da die Stelligkeit eines Primitivs dem Primitiv fest zugeordnet
ist, ist eine Hilfsfunktion nützlich, die bei der Erzeugung eines
Werts der Sorte \texttt{prim} die Stelligkeit ergänzt.
Glücklicherweise haben alle oben eingeführten Primitive die gleiche
Stelligkeit:
%
\begin{verbatim}
; Primitiv erzeugen
(: make-prim (symbol -> prim))
(define make-prim
(lambda (s)
(real-make-prim s 2)))
\end{verbatim}
%
Die Einführung von Primitive mit anderen Stelligkeiten ist Gegenstand
von Aufgabe~\ref{aufgabe:prim-arity}.
\subsection{Übersetzung in Maschinencode}
Nun, da sowohl Terme als auch der Maschinencode Datendefinitionen
haben, ist es möglich, die Übersetzung zu programmieren. Hier sind
Kurzbeschreibung, Signatur und Gerüst:
%
\begin{verbatim}
; Term in Maschinencode übersetzen
(: term->machine-code (term -> machine-code))
(define term->machine-code
(lambda (e)
...))
\end{verbatim}
%
Da es sich bei \texttt{term} um gemischte Daten handelt, muss~-- wie
immer~-- eine Verzweigung den Rumpf der Funktion bilden:
%
\begin{verbatim}
(define term->machine-code
(lambda (e)
(cond
((symbol? e) ...)
((application? e) ...)
((abstraction? e) ...)
((base? e) ...)
((primitive-application? e) ...))))
\end{verbatim}
%
Die Implementierung entspricht in den einzelnen Fällen genau der
Übersetzungsfunktion $\llbracket\underline{~}\rrbracket$. Die Fälle
für Variablen und Basiswerte sind, genau wie dort, trivial:
%
\begin{verbatim}
(define term->machine-code
(lambda (e)
(cond
((symbol? e) (list e))
((base? e) (list e))
...)))
\end{verbatim}
%
Bei regulären Applikationen werden
Operator und Operand übersetzt, und das ganze zusammen mit einer
\texttt{ap}-Instruktion zu einer Liste zusammengesetzt:
%
\begin{verbatim}
(define term->machine-code
(lambda (e)
(cond
...
((application? e)
(append (term->machine-code (first e))
(append (term->machine-code (first (rest e)))
(list (make-ap)))))
...)))
\end{verbatim}
%
Bei den primitiven Applikationen werden erst einmal die Operanden in
Maschinencode übersetzt, die Resultate aneinandergehängt, und
schließlich kommt noch eine \texttt{prim}-Instruktion ans Ende:
%
\begin{verbatim}
(define term->machine-code
(lambda (e)
(cond
...
((primitive-application? e)
(append
(append-lists
(map term->machine-code (rest e)))
(list (make-prim (first e)))))
...)))
\end{verbatim}
%
Dieses Stück Code benutzt die Hilfsfunktion \texttt{append-lists}, die
aus einer Liste von Listen eine einzelne Liste macht, indem die
Elemente aneinandergehängt werden:
%
\begin{verbatim}
; die Elemente einer Liste von Listen aneinanderhängen
(: append-lists ((list-of (list-of %a)) -> (list-of %a)))
(define append-lists
(lambda (l)
(fold '() append l)))
\end{verbatim}
%
Zurück zur Übersetzung: Eine Abstraktionen wird direkt in eine
\texttt{abs}-Instruktion übersetzt, wobei der Rumpf selbst
noch in Maschinencode übersetzt wird:
%
\begin{verbatim}
(define term->machine-code
(lambda (e)
(cond
...
((abstraction? e)
(list
(make-abs (first (first (rest e)))
(term->machine-code
(first (rest (rest e))))))))))
\end{verbatim}
%
\subsection{Zustandsübergang und Auswertung}
\label{sec:secd-transition}
Da nun alle $\lambda$-Terme in Maschinencode-Programme übersetzt
werden können, ist jetzt die eigentliche SECD-Maschine an der Reihe.
Hier sind erst einmal einige neue Datendefinitionen fällig. Zunächst
einmal die Menge $S$ der Stacks:
%
\begin{verbatim}
; Ein Stack ist eine Liste von Werten
(define stack (signature (list-of value)))
\end{verbatim}
%
Die Definition von Werten $W$ kommt etwas später an die Reihe.
Umgebungen aus der Menge $E$ sind mathematisch gesehen Mengen aus
Tupeln. In der Implementierung werden sie dargestellt aus Listen von
\textit{Bindungen\index{Bindung}}, wobei jede Bindung einem Tupel aus
der mathematischen Definition entspricht:
\begin{verbatim}
; Eine Umgebung ist eine Liste von Bindungen.
; Dabei gibt es für jede Variable nur eine Bindung.
(define environment (signature (list-of binding)))