|
%------------------------------------------------------------------------------
% Admissible Predicates
%
% Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% If a predicate is "admissible" then we have an induction principle for
% fixpoints (fixpoint_induction).
%
% Version 1.0 1/11/06 Initial Version
%------------------------------------------------------------------------------
admissible[T:TYPE+, (IMPORTING orders@directed_orders[T])
<=:(pointed_directed_complete_partial_order?[T])]: THEORY
BEGIN
IMPORTING fixpoints[T,<=]
x: VAR T
D: VAR set[T]
q: VAR pred[T]
phi: VAR (increasing?[T,T,<=,<=])
% An admissible predicate is a lub-preserving function between T and the
% special two-point pointed DCPO: TRUE < FALSE, that is also TRUE for bottom.
IMPORTING scott[bool,when], scott_continuity[T,bool,<=,when]
admissible_pred?(p:pred[T]):bool
= FORALL D: empty?(D) OR directed?(D) => (FORALL (x:(D)): p(x)) => p(lub(D))
admissible_pred: TYPE+ = (admissible_pred?) CONTAINING (LAMBDA x: TRUE)
p: VAR admissible_pred
fixpoint_induction: LEMMA (FORALL x: p(x) => p(phi(x))) => p(fix(phi))
END admissible
¤ Dauer der Verarbeitung: 0.14 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.
|
