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) elselet (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 ANDFORALL (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 ELSELET n = log_nat_it(1/xp,2)`1 IN -n ENDIF
END log_nat
¤ Dauer der Verarbeitung: 0.12 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.
