% if <= is a complete lower semilattice on T and f is a monotone function from
% T to T, then f is a least fixed point of x iff f is the least prefixed point.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Nov 2004
fixed_points[T: TYPE+]: THEORY
BEGIN
IMPORTING minmax_orders[T]
R: VAR pred[[T, T]]
<=: VAR (complete_lower_semilattice?[T])
x, y: VAR T
f: VAR [T -> T]
monotone?(R)(f): bool = FORALL x, y: R(x, y) => R(f(x), f(y))
fixed_point?(f)(x): bool = (f(x) = x)
prefixed_point?(R)(f)(x): bool = R(f(x), x)
lfp?(R)(f)(x): bool = least?(fixed_point?(f), R)(x)
prefixed_points_closed: LEMMA
FORALL (f: (monotone?(<=))):
prefixed_point?(<=)(f)(x) => prefixed_point?(<=)(f)(f(x))
prefixed_points_lower_bounds: LEMMA
FORALL (f: (monotone?(<=))):
lower_bound?[T](x, prefixed_point?(<=)(f), <=) =>
lower_bound?[T](f(x), prefixed_point?(<=)(f), <=)
least_prefixed_point_is_fixed_point: LEMMA
FORALL (f: (monotone?(<=))):
greatest_lower_bound?[T](x, prefixed_point?(<=)(f), <=) =>
fixed_point?(f)(x)
least_fixed_point_le_prefixed_points: LEMMA
FORALL (f: (monotone?(<=))):
lfp?(<=)(f)(x) => lower_bound?[T](x, prefixed_point?(<=)(f), <=)
least_prefixed_point: THEOREM
FORALL (f: (monotone?(<=))):
lfp?(<=)(f)(x) IFF greatest_lower_bound?[T](x, prefixed_point?(<=)(f), <=)
least_fixed_point_exists: COROLLARY
FORALL (f: (monotone?(<=))):
nonempty?(lfp?(<=)(f))
least_fixed_point_unique: COROLLARY
FORALL (f: (monotone?(<=))):
unique?(lfp?(<=)(f))
END fixed_points
¤ Dauer der Verarbeitung: 0.21 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.
|
