|
top_sigma: THEORY
%------------------------------------------------------------------------------
% The sigma theory introduces and defines properties of the sigma
% function that sum an arbitrary function F: [T -> real] over a range
% from low to high
%
% high
% ----
% sigma(low, high, F) = \ F(j)
% /
% ----
% j = low
%
% and alternate (tail recursion) form
%
% high
% ----
% sum_it(low, high, F, a )= a + \ F(j)
% /
% ----
% j = low
%
%
%
% by Ricky W. Butler NASA Langley
% Cesar Munoz Langley ICASE
% Paul Miner NASA Langley
%
% Version 1.0 original version 7/12/96
% Version 2.0 4/2/01
%
%
% NOTE: T can be any subtype of the integers that is connected. For
% example "subrange(-12,7)", nat, or posnat.
%
% NOTE: Summations over functions with an arbirary number of arguments
% is accomodated by the following technique:
%
% G(x,y,z: real,n: nat): real
%
% IMPORTING sigma[nat] % or sigma_nat
%
% sum = sigma(low,high, (LAMBDA (n:nat): G(x,y,z,n))
%
% NOTE: The old library "sigma_real" is now subsumed by sigma_nat.
%
% NOTE: "sigma_real.sigma_mult" is named "sigma_scal" in "sigma"
%------------------------------------------------------------------------------
BEGIN
IMPORTING sigma, % generic theory
sigma_nat, % sigma over functions [nat --> real]
sigma_posnat, % sigma over functions [posnat --> real]
sigma_int, % sigma over functions [int --> real]
sigma_upto, % sigma over functions [upto[N] --> real]
sigma_below, % sigma over functions [below[N] --> real]
sigma_below_sub, % equality of sigmas with different domains
sigma_fseq_def, % summation over finite sequences
sigma_fseq % Bug prevents typecheck
% The more specific theories have stronger theorems than the generic one
%% ------- Following Obsolete
% old_sigma_below,
% old_sigma_below_sub,
% old_sigma_int,
% old_sigma_nat,
% old_sigma_posnat,
% old_sigma,
% old_sigma_real,
% old_sigma_upto
END top_sigma
¤ Dauer der Verarbeitung: 0.25 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.
|
