%------------------------------------------------------------------------------
% The Equivalence of a Direct and Continuation Semantics
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
congruence[V:
TYPE+]:
THEORY
BEGIN
IMPORTING direct[V], continuation[V],
scott@admissible[Cont,sq_le],
scott@admissible[(scott_continuous?[Cont,Cont,sq_le,sq_le]),
(continuous_pointwise(sq_le,sq_le))]
s:
VAR State
c:
VAR Cont
S:
VAR Stm
phi:
VAR scott_continuous[Cont,Cont,(sq_le),(sq_le)]
psi:
VAR Cont
P(phi,psi):bool =
FORALL c: phi(c) = c
o psi
P_bottom:
LEMMA P(
LAMBDA c:
LAMBDA s: bottom[State],
LAMBDA s: bottom[State])
IMPORTING
orders@product_orders[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont],
scott@scott_continuity[[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont],
bool,(continuous_pointwise(sq_le,sq_le)*sq_le),
when],
scott@dual_fixpoints[(scott_continuous?[Cont,Cont,(sq_le),(sq_le)]),Cont,
continuous_pointwise(sq_le,sq_le),sq_le]
admissible_P:
LEMMA admissible_pred?(P)
continuation_direct:
LEMMA P(continuation.SS(S),direct.SS(S))
% N&N 4.74
END congruence
