|
%------------------------------------------------------------------------------
% Definition and properties of Fixpoints
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Note carefully:
%
% FIX(f) is the set of all fixpoints of any function.
% fix(phi) is the least fixpoint of an increasing (ie monotonic) function.
%
% And especially: only when the function (psi) is continuous do we have
%
% psi(fix(psi)) = fix(psi)
%
% Version 1.0 25/12/07 Initial Version
%------------------------------------------------------------------------------
fixpoints[T:TYPE+, (IMPORTING orders@directed_orders[T])
<=:(pointed_directed_complete_partial_order?[T])]: THEORY
BEGIN
IMPORTING fun_preds_partial[T,T,<=,<=],
orders@directed_order_props[T,<=]
n: VAR nat
x,y: VAR T
f,g: VAR [T -> T]
phi: VAR (increasing?)
X: VAR (nonempty?[T])
D: VAR directed
unique_bottom: LEMMA least?(fullset[T],<=)(x) AND
least?(fullset[T],<=)(y) IMPLIES x = y
bottom: (least?(fullset[T],<=))
bottom_le: LEMMA bottom <= x
le_bottom: LEMMA (x <= bottom) IMPLIES x = bottom
nonempty_T: LEMMA nonempty?(fullset[T])
IMPORTING algebra@monoid[[T->T],function_props[T,T,T].o,(LAMBDA x: x)],
scott[T,<=],
orders@chain[T,<=],
fun_preds_partial[nat,T,reals.<=,<=]
FIX_APPROX(phi):set[T] = image((LAMBDA n: power(phi,n)(bottom)),fullset[nat])
FIX(f) :set[T] = {x | f(x) = x}
lub_add_bottom: LEMMA lub(D) = lub(add(bottom,D))
increasing_phi_n: LEMMA increasing?(power(phi,n))
increasing_power: LEMMA increasing?(LAMBDA n: power(phi,n)(bottom))
fix_approx_nonempty: LEMMA nonempty?(FIX_APPROX(phi))
fix_approx_chain: LEMMA chain?(FIX_APPROX(phi))
ne_chain_is_directed: LEMMA chain?(X) IMPLIES directed?(<=)(X)
lub_emptyset: LEMMA lub(emptyset[T]) = bottom
fix(phi):T = lub(FIX_APPROX(phi))
member_FIX: LEMMA member(x,FIX(f)) IMPLIES f(x) = x
fix_is_least: LEMMA member(x,FIX(phi)) IMPLIES fix(phi) <= x
fix_le: LEMMA fix(phi) <= phi(fix(phi))
IMPORTING scott_continuity[T,T,<=,<=]
psi: VAR (continuous?)
fix_in_FIX: LEMMA member(fix(psi),FIX(psi))
nonempty_FIX: LEMMA nonempty?(FIX(psi))
fix_prop: LEMMA psi(fix(psi)) = fix(psi)
fixpoint_contraction: LEMMA psi(x) <= x => fix(psi) <= x
END fixpoints
¤ Dauer der Verarbeitung: 0.4 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.
|
