%------------------------------------------------------------------------------ % Top for Scott Topology % % All references are to BA Davey and HA Priestly "Introduction to Lattices and % Orders", CUP, 1990. % % This library defines the Scott Topology, and shows that continuous functions % are increasing and lub-preserving; and -- under pointwise-ordering -- also % form a Scott Topology. % % The main reason Computer Scientists are interested is that it constitutes a % general foundation on which to build the fixpoint theory needed for the % semantics of loops or recursion. % % Author: David Lester, Manchester University, NIA, Université Perpignan % % Version 1.0 25/12/07 Initial Version %------------------------------------------------------------------------------
top: THEORY
BEGIN
IMPORTING
partial_function_props, % Easy-to-use partial function properties
scott, % Definition of Scott Topology
scott_continuity, % Definition of Continuity
pointwise_orders_aux, % Extras for continuous pointwise orders
scott_identity_continuity, % Identity is scott continuous
scott_composition_continuity, % Composition is scott continuous
fixpoints, % Definition of Fixpoints
admissible, % Fixpoint induction
dual_fixpoints, % Fixpoint Induction over two types
scott_product
% Extras for orders library %% INTEGRATED %% % % bounded_orders_aux, % Extras for orders@bounded_orders % ordered_subset_aux, % Extras for orders@ordered_subset % % New Theory files for orders library %% MOVED %% % % lift_props, % Extras for the lift datatype % directed_orders, % New theories for orders library % bounded_order_props, % Properties of bounded orders % directed_order_props, % Properties of directed orders % partial_order_props, % Properties of partial orders % partial_order_lift % lifted_orders, % Induced properties of lifted orders % sum_orders, % Induced properties of union orders % product_orders % Induced properties of product orders
END top
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
