Contexts simplified

In previous work on TransLucid, it was never clear whether a context was a finite or an infinite object. Well, it turns out that by making it an infinite object, then the semantics is a lot cleaner, and bestfitting will become simpler as well. This is the way that it works. Let D be the domain of atomic values. Then a context κ is an element of K = D to D, and a set of contexts K is a subset of K. Then the denotational semantics of TransLucid expressions is much more easily expressed. Here it is, ignoring identifiers and undefined values:


⟦c⟧σκ = c
⟦op(E1, ..., En)⟧σκ = op(⟦E1⟧σκ, ..., ⟦En⟧σκ)
⟦if E1 then E2 else E3⟧σκ = if ⟦E1⟧σκ then ⟦E2⟧σκ else ⟦E3⟧σκ
⟦#E⟧σκ = κ(⟦E⟧σκ)
⟦E11:E12, ..., En1:En2⟧σκ = {⟦E11⟧σκ ⟼ ⟦E12⟧σκ, ..., ⟦En1⟧σκ ⟼ ⟦En2⟧σκ}
⟦E2 @ E1⟧σκ = ⟦E2⟧σ(κ † ⟦E1⟧σκ)

Advertisement