|
mucalculus_prop [ T:TYPE ] : THEORY
%-------------------------------------------------------------------
% Fixed points of monotonic functions of type [set[T] -> set[T]]
% (predicate transformers)
%
% Shows that operators mu and nu defined in theory mucalculus
% of the prelude defines the least and greatest fixpoints of
% a monotonic function
%
% Defines dual(H) = complement o H o complement
%
% Shows that mu o dual = complement o nu and
% nu o dual = complement o mu
%-------------------------------------------------------------------
BEGIN
F: VAR (monotonic?[T])
p, q: VAR pred[T]
A: VAR set[pred[T]]
% Auxiliary functions defined in the prelude (theory mucalculus):
% - relation <= is the same as the subset? relation
% - glb(A) = { x:T | EXISTS (p: (A)): p(x) }
% - lub(A) = { x:T | FORALL (p: (A)): p(x) }
antisymmetry: LEMMA p <= q AND q <= p IMPLIES p = q
reflexivity: LEMMA p <= p
%--- glb(A) is the greatest lower bound of A
glb_lower_bound: LEMMA FORALL (q: (A)): glb(A) <= q
glb_greatest_lower_bound: LEMMA
p <= glb(A) IFF FORALL (q: (A)): p <= q
%--- lub(A) is the least upper bound of A
lub_upper_bound: LEMMA FORALL (q: (A)): q <= lub(A)
lub_least_upper_bound: LEMMA
lub(A) <= p IFF FORALL (q: (A)): q <= p
%--- properties of mu operator
closure_mu: PROPOSITION F(mu(F)) <= mu(F)
smallest_closed: PROPOSITION F(p) <= p IMPLIES mu(F) <= p
fixpoint_mu1: PROPOSITION F(mu(F)) = mu(F)
fixpoint_mu2: PROPOSITION fixpoint?(F)(mu(F))
least_fixpoint1: PROPOSITION F(p) = p IMPLIES mu(F) <= p
least_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES mu(F) <= p
mu_lfp: JUDGEMENT mu(F) HAS_TYPE (lfp?(F))
%--- properties of nu operator
closure_nu: PROPOSITION nu(F) <= F(nu(F))
largest_closed: PROPOSITION p <= F(p) IMPLIES p <= nu(F)
fixpoint_nu1: PROPOSITION F(nu(F)) = nu(F)
fixpoint_nu2: PROPOSITION fixpoint?(F)(nu(F))
greatest_fixpoint1: PROPOSITION F(p) = p IMPLIES p <= nu(F)
greatest_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES p <= nu(F)
nu_gfp: JUDGEMENT nu(F) HAS_TYPE (gfp?(F))
%--- dual of a predicate transformer
H: VAR [pred[T] -> pred[T]]
dual(H): [pred[T] -> pred[T]] = complement o H o complement
dual_dual : LEMMA dual(dual(H)) = H
dual_inclusion1 : LEMMA
H(complement(p)) <= complement(p) IFF p <= dual(H)(p)
dual_inclusion2 : LEMMA
complement(p) <= H(complement(p)) IFF dual(H)(p) <= p
dual_inclusion3 : LEMMA
H(p) <= p IFF complement(p) <= dual(H)(complement(p))
dual_inclusion4 : LEMMA
p <= H(p) IFF dual(H)(complement(p)) <= complement(p)
%--- fixed points and dual
monotonic_dual_monotonic: JUDGEMENT dual(F) HAS_TYPE (monotonic?[T])
least_fixpoint_dual: PROPOSITION mu(dual(F)) = complement(nu(F))
greatest_fixpoint_dual: PROPOSITION nu(dual(F)) = complement(mu(F))
END mucalculus_prop
¤ Dauer der Verarbeitung: 0.1 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.
|
