This project is young and has never been used in production before. Expect to help find and report bugs if you use this project.

Zero equivalence of log-exp functions is undecidable and reducible to computing symbolic limits. Specifically, to determine if the expression x is zero, compute the limit limit(ϵ/(x + ϵ), ϵ, 0), which is 1 if x == 0 and 0 if x != 0. This package implements a reduction in the reverse direction, and always produces an answer and terminates. To avoid the undecidability issue, SymbolicLimits utilizes a heuristic iszero detector and, tracks all its results as assumptions. The returned result is correct if the assumptions all hold. In practice, the heuristic is pretty good and the assumptions typically all hold.

The limit function is the whole of the public API of this package.

limit(expr, var, h[, side::Symbol])

Compute the limit of expr as var approaches h and return (limit, assumptions). If all the assumptions are true, then the returned limit is correct.

side indicates the direction from which var approaches h. It may be one of :left, :right, or :both. If side is :both and the two sides do not align, an error is thrown. Side defaults to :both for finite h, :left for h = Inf, and :right for h = -Inf.

using Pkg; pkg"activate --temp"; pkg"add https://github.com/LilithHafner/SymbolicLimits.jl"; pkg"add SymbolicUtils" # slow

using SymbolicLimits, SymbolicUtils # slow

@syms x::Real

limit(exp(x+exp(-x))-exp(x), x, Inf)[1] == 1 # slow

# the rest is fast

limit(-1/x, x, Inf)[1]
limit(-x / log(x), x, Inf)[1]
limit(exp(x+exp(-x))-exp(x), x, Inf)[1]
limit(x^7/exp(x), x, Inf)[1]
limit(x^70000/exp(x), x, Inf)[1]
limit(log(log(x*exp(x*exp(x))+1))-exp(exp(log(log(x))+1/x)), x, Inf)[1]