% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
