%------------------------------------------------------------------------------
% Properties of Lifted Orders
%
% Author: David Lester <[email protected]> Manchester University
%
% We define a lifting operator on relations, and show that this operation
% preserves directed completeness and pointedness.
%
% Version 1.0 03/30/06
%------------------------------------------------------------------------------
lifted_orders[T:TYPE]: THEORY
BEGIN
rel: VAR pred[[T,T]]
x,y: VAR lift[T]
IMPORTING lift_props[T]
lift(rel)(x,y):bool = (NOT up?(x)) OR (up?(y) AND rel(down(x),down(y)))
lift_preserves_reflexive: JUDGEMENT
lift(r:(reflexive?[T])) HAS_TYPE (reflexive?[lift[T]])
lift_preserves_transitive: JUDGEMENT
lift(r:(transitive?[T])) HAS_TYPE (transitive?[lift[T]])
lift_preserves_antisymmetric: JUDGEMENT
lift(r:(antisymmetric?[T])) HAS_TYPE (antisymmetric?[lift[T]])
lift_preserves_preorder: JUDGEMENT
lift(r:(preorder?[T])) HAS_TYPE (preorder?[lift[T]])
lift_preserves_partial_order: JUDGEMENT
lift(r:(partial_order?[T])) HAS_TYPE (partial_order?[lift[T]])
IMPORTING directed_orders[T], directed_orders[lift[T]]
lift_lub_emptyset: LEMMA lub(lift(rel))(emptyset[lift[T]]) = bottom
lift_lub_bounded: LEMMA FORALL (rel:(antisymmetric?[T]),
S:(nonempty_least_bounded_above?(rel))):
lub(lift(rel))(image[T,lift[T]](up,S)) = up(lub(rel)(S))
lift_preserves_directed_complete: JUDGEMENT
lift(r:(directed_complete?[T])) HAS_TYPE (directed_complete?[lift[T]])
lift_preserves_directed_complete_partial_order: JUDGEMENT
lift(r:(directed_complete_partial_order?[T]))
HAS_TYPE (pointed_directed_complete_partial_order?[lift[T]])
END lifted_orders
¤ Dauer der Verarbeitung: 0.0 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.
|
