Average Error: 29.2 → 0.0
Time: 4.9s
Precision: binary64
Cost: 6592
\[\log \left(N + 1\right) - \log N \]
↓
\[\mathsf{log1p}\left(\frac{1}{N}\right) \]
(FPCore (N) :precision binary64 (- (log (+ N 1.0)) (log N)))
↓
(FPCore (N) :precision binary64 (log1p (/ 1.0 N)))
double code(double N) {
	return log((N + 1.0)) - log(N);
}
↓
double code(double N) {
	return log1p((1.0 / N));
}

public static double code(double N) {
	return Math.log((N + 1.0)) - Math.log(N);
}
↓
public static double code(double N) {
	return Math.log1p((1.0 / N));
}

def code(N):
	return math.log((N + 1.0)) - math.log(N)
↓
def code(N):
	return math.log1p((1.0 / N))

function code(N)
	return Float64(log(Float64(N + 1.0)) - log(N))
end
↓
function code(N)
	return log1p(Float64(1.0 / N))
end

code[N_] := N[(N[Log[N[(N + 1.0), $MachinePrecision]], $MachinePrecision] - N[Log[N], $MachinePrecision]), $MachinePrecision]
↓
code[N_] := N[Log[1 + N[(1.0 / N), $MachinePrecision]], $MachinePrecision]

\log \left(N + 1\right) - \log N
↓
\mathsf{log1p}\left(\frac{1}{N}\right)

Error

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 29.2

    \[\log \left(N + 1\right) - \log N \]

  2. Simplified29.2

    \[\leadsto \color{blue}{\mathsf{log1p}\left(N\right) - \log N} \]
    Proof
    (-.f64 (log1p.f64 N) (log.f64 N)): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 N))) (log.f64 N)): 1 points increase in error, 0 points decrease in error
    (-.f64 (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 N 1))) (log.f64 N)): 0 points increase in error, 0 points decrease in error

  3. Applied egg-rr29.1

    \[\leadsto \color{blue}{\log \left(\frac{N + 1}{N}\right)} \]

  4. Applied egg-rr29.1

    \[\leadsto \log \color{blue}{\left(1 + \left(\frac{N + 1}{N} - 1\right)\right)} \]

  5. Simplified29.1

    \[\leadsto \log \color{blue}{\left(\left(1 + \frac{1}{N}\right) + 0\right)} \]
    Proof
    (+.f64 (+.f64 1 (/.f64 1 N)) 0): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 1 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 1 N) 1))) 0): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (Rewrite<= lft-mult-inverse_binary64 (*.f64 (/.f64 1 N) N)) (*.f64 (/.f64 1 N) 1)) 0): 0 points increase in error, 18 points decrease in error
    (+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 (/.f64 1 N) (+.f64 N 1))) 0): 1 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (+.f64 N 1)) N)) 0): 19 points increase in error, 2 points decrease in error
    (+.f64 (/.f64 (Rewrite=> *-lft-identity_binary64 (+.f64 N 1)) N) 0): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (+.f64 N 1) N) (Rewrite<= metadata-eval (-.f64 1 1))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (+.f64 N 1) N) 1) 1)): 3 points increase in error, 1 points decrease in error
    (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (/.f64 (+.f64 N 1) N))) 1): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate--l+_binary64 (+.f64 1 (-.f64 (/.f64 (+.f64 N 1) N) 1))): 1 points increase in error, 3 points decrease in error

  6. Applied egg-rr0.0

    \[\leadsto \color{blue}{0 + \mathsf{log1p}\left(\frac{1}{N}\right)} \]

  7. Simplified0.0

    \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{N}\right)} \]
    Proof
    (log1p.f64 (/.f64 1 N)): 0 points increase in error, 0 points decrease in error
    (Rewrite<= +-lft-identity_binary64 (+.f64 0 (log1p.f64 (/.f64 1 N)))): 0 points increase in error, 0 points decrease in error

  8. Final simplification0.0

    \[\leadsto \mathsf{log1p}\left(\frac{1}{N}\right) \]

Reproduce

herbie shell --seed 2022334 
(FPCore (N)
  :name "2log (problem 3.3.6)"
  :precision binary64
  (- (log (+ N 1.0)) (log N)))