%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
