| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle fixed_points.pvs Sprache: PVS |
|||||||||
|
% 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 (geser@nianet.org), 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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28