|
log_nat : THEORY
%----------------------------------------------------------------------------
%
% Authors: Cesar Munoz (NIA)
% This theory implements an algorithm to compute the natural part and the
% real part of a logarithm. This algorithm is analogous to the Euclidean
% division procedure.
% Date: March 28 2005
%
%----------------------------------------------------------------------------
BEGIN
x,y,ya : VAR {x:real| x >= 1}
na : VAR nat
p : VAR above(1)
IMPORTING prelude_aux
log_nat(x,p): RECURSIVE [n:nat,{y | y<p AND x=p^n*y}] =
if x < p then (0,x)
else let (n,y) = log_nat(x/p,p) in (n+1,y)
endif
MEASURE floor(x)
log_nat_bounds : LEMMA
let (n,y)=log_nat(x,p) in
p^n <= x AND x < p^(n+1)
log_nat_incr : LEMMA
p*x <= y IMPLIES
log_nat(x,p)`1 < log_nat(y,p)`1
log_nat_itaux(x,p,na,(ya | x=p^na*ya)): RECURSIVE [n:nat,{y | y<p AND x=p^n*y}] =
if ya < p then (na,ya)
else log_nat_itaux(x,p,na+1,ya/p)
endif
MEASURE floor(ya)
log_nat_it(x,p) : [n:nat,{y | y <p AND x=p^n*y}] =
log_nat_itaux(x,p,0,x)
log_nat_id : LEMMA
log_nat_it(x,p) = log_nat(x,p)
least_pow_2_ge(xp:posreal): {k:int |
xp<=2^k AND FORALL (i:int): i<k IMPLIES 2^i<xp} =
IF xp>=1 THEN
LET (n,y) = log_nat_it(xp,2) IN
IF y=1 THEN n
ELSE n+1 ENDIF
ELSIF xp>1/2 THEN 0
ELSE LET n = log_nat_it(1/xp,2)`1 IN -n ENDIF
END log_nat
¤ Dauer der Verarbeitung: 0.12 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.
|
