昨日のエントリで、Kleisli構成により「関数やメソッドのようなdenotationalな対象ではなくて、コード（プログラム字面）そのもの、構文的な対象」を射とするような圏ができる、といったけど、そういうものをopen programsと呼ぶことがあるようだ。
open programは、Kleisli射の逆（opposite）のことだと定義していいだろう。つまり、p:Γ→L(Σ) in Sign を p:Σ→Γ in OpenProgram と解釈する。Γ上の文（論理式）は、pを使ってマクロ展開できて、L(Σ)上の文になる。だから、文のレベルでは p*:Sen(Γ)→Sen(L(Σ)) がinduceされる。p*は翻訳だな。
翻訳p*が演繹系のあいだの健全（sound）な翻訳になっていることが、open program pの“正しさ”の定義になるだろう。
