|
%------------------------------------------------------------------------------
% 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.16 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.
|
