Continuation Semantics for PROLOG with Cut

摘要

A denotational continuation semantics for PROLOG with cut is presented. First a uniform language B is studied, which captures the control flow aspects of PROLOG. The denotational semantics for B is proven equivalent to a transition system based on operational semantics. The congruence proof relies on the representation of the operational semantics as a chain of approximations and on a convenient induction principle. Finally, the abstract language B is interpreted such that equivalent denotational and operational models are obtained for PROLOG itself.