![[^]](IS.GIF){kind=small}
Übersicht ![[+]](IL.GIF){kind=small}
Folie 11 ![[+]](IR.GIF){kind=small}
Folie 13 | Übersicht Folie 11 Folie 13 | Beweis der 1. Futamura-Projektion |
| Gegeben: |
ein S-Interpreter int geschrieben in L, ein S-Programm s und seine Eingabedaten d |
||
| Behauptung: | Die 1. Futamura-Projektion entspricht dem Effekt der Compilierung | ||
| Beweis: | |||
| ||s||S d | = ||int||L [s, d] |
nach Definition eines Interpreters | |
| = ||(||mix||L [int, s] )||L d | nach der mix Gleichung | ||
| = ||target||L d | nach Umbenennung des residualen Programms in target |