§ Bootstrapping and self-application

• Suppose we have a high-level compiler in the language S, from S to T. I will denote that as h : S(S → T). where the compiler is h (for high), written in language S, from S to T.
• We also have a low-level compiler written in T from S to T, denoted by l : T(S → T), where the compiler is l for low.
• Suppose the two versions agree, so [h]_S = [l]_T.
• Suppose we extend h to h', to compile the language S' to T. h' is also written in S, so we have h': S(S'→ T).
• Now we can use t on h' to recieve an S' compiler l' : T(S' → T).