ページ記述言語プログラムの等価性に関する一考察 On Proving Equivalence of Programs in Page Description Languages

文書構造を表すプログラミング言語の一つにページ記述言語がある.我々はページ記述言語Interpressに操作的意味を与え,その意味にしたがってInterpressのプログラムをPostScriptで解釈する方法を確立した.さらにその技法を用いて,InterpressからPostScriptへ自動的に変換するソフトウェアip2psを作成した.本稿では,ip2psの変換等価性をモナドを用いた圈論的意味論で示すことを試みた.

A page description language is a programming language for representations of document structures. We present the operational semantics for Interpress, which is one of page description languages, and the techniques of interpreting Interpress with PostScript based on this semantics. Ip2ps which is derived from these techniques is an automatic program transformation software from Interpress program to PostScript one. In this paper we try to prove the equivalence of programs on ip2ps using a categorical semantics with monads.