An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. (Q1853149)

We show that any \(\lambda\)-model gives rise to a \(\lambda \mu\)-model, in the sense that if we have \(M=_{\lambda \mu}N\) in the equational theory of type free \(\lambda \mu\)-calculus then \([[M]]=_{D}[[N]]\) holds true for some structure \(\langle [[-]],D\rangle\) induced from a \(\lambda\)-model. The construction of \(\lambda \mu\)-models can be given by the use of a fixed point operator and the Gödel--Gentzen translation.