Differentiate an abstract exponential and refine its values

Construct an abstract expression

The abstract function retains its semantic identity and characterization even when it has no evaluation algorithm:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); Exp := .calculus.Exp(); expression := 3 * Exp(x^2 + 1); .Table({= columns=["kind", "schema", "operation"], rows=[[ expression[:kind], expression[:schema], expression[:operation] ]] });

Inspect Exp.Record(). Its facts field records both y' = y and the initial condition y(0) = 1; its hasImplementation field is null.

Cross the public specification boundary

The portable graph can become a core symbolic specification and return without losing the exponential's semantic ID:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); Exp := .calculus.Exp(); expression := 3 * Exp(x^2 + 1); specification := .calculus.ToSpec(expression, [:x]); restored := .calculus.FromSpec(specification); .Table({= columns=["specification", "restored kind", "semantic function"], rows=[[ specification, restored[:kind], restored[:operands][1][:semanticId] ]] });

The core specification remains inert for semantic applications. Calculus can nevertheless resolve the retained semantic ID through its rule registry.

Differentiate by semantic identity

Exp registers its exact outer derivative separately from any numerical implementation. Arithmetic and chain rules build another portable graph:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); Exp := .calculus.Exp(); expression := 3 * Exp(x^2 + 1); derivative := .calculus.Differentiate(expression, :x); entry := .calculus.Resolve(Exp); .Table({= columns=["derivative", "semantic ID", "rule evidence"], rows=[[ .calculus.ToSpec(derivative), entry[:semanticId], entry[:evidence][:derivative][:identity] ]] });

The derivative is exact because the registry contains D Exp = Exp and the ordinary product, power, and chain rules apply. Finite differences or sampled values never become exact derivative evidence.

Keep domain and branch obligations with the result

Some exact formulas are conditional. Use DifferentiateResult to keep the derivative, the conditions under which it is valid, and its rule evidence in one transformation record:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); logResult := .calculus.DifferentiateResult(.calculus.Log()(x^2), :x); sqrtResult := .calculus.DifferentiateResult(.calculus.Sqrt()(x), :x); asinResult := .calculus.DifferentiateResult(.calculus.Asin()(x), :x); complexResult := .calculus.DifferentiateResult(.calculus.ComplexLog()(x), :x); .Table({= columns=["function", "derivative", "kind", "required relation"], rows=[ ["Log", .calculus.ToSpec(logResult[:expression]), logResult[:obligations][1][:kind], logResult[:obligations][1][:relation]], ["Sqrt", .calculus.ToSpec(sqrtResult[:expression]), sqrtResult[:obligations][1][:kind], sqrtResult[:obligations][1][:relation]], ["Asin", .calculus.ToSpec(asinResult[:expression]), asinResult[:obligations][1][:kind], asinResult[:obligations][1][:relation]], ["ComplexLog", .calculus.ToSpec(complexResult[:expression]), complexResult[:obligations][1][:kind], complexResult[:obligations][1][:relation]] ] });

The real rules retain positivity or open-interval requirements. The complex rule retains the selected principal branch and its branch cut. The convenience .calculus.Differentiate(...) form deliberately errors for these examples; it returns a bare expression only when the obligation list is empty.

Operators participate in the same contract. This quotient result records that its original denominator must remain nonzero:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); result := .calculus.DifferentiateResult((x+1)/(x-1), :x); {: .calculus.ToSpec(result[:expression]), result[:obligations] };

Custom semantic rules use the same mechanism: register derivative and a separate derivativeObligations callable returning values made with .calculus.Obligation(...). This keeps a formula, its preconditions, and the evidence for each in distinct registry slots.

Runnable RiXRun cell

.Plugin.Load("calculus"); PositiveOnly := .calculus.Function("example.positive-only@1", {= name=:PositiveOnly, domain=:positiveReal, codomain=:real }); .calculus.Register(PositiveOnly, {= derivative=(application)->1, derivativeObligations=(application)->[ .calculus.Obligation(:domain,:positive,application[:arguments][1], {= reason=:customPositiveDomain }) ], derivativeEvidence=:definition }); x := .calculus.Variable(:x); result := .calculus.DifferentiateResult(PositiveOnly(x^2), :x); {: .calculus.ToSpec(result[:expression]), result[:obligations] };

Move form-preserving rational functions into Calculus

The Symbolic workspace loads Calculus and exposes the public bridge. A FractionFunction contributes both its expression and its original denominator restrictions:

Runnable RiXRun cell

.Plugin.Load("symbolic"); F := .ff`(x^2-1)/(x-1)`; C := F.Cancel(); derivative := .symbolic.DifferentiateResult(F, :x); .Table({= columns=["display form", "cancelled display", "source expression", "source obligations"], rows=[[ .calculus.ToSpec(F.CalculusExpression()), .calculus.ToSpec(C.CalculusExpression()), .calculus.ToSpec(C.EvaluationCalculusExpression()), .symbolic.Obligations(C) ]] });

Cancellation changes the displayed expression but not the source-domain hole. The public Calculus view makes that distinction available to other plugins without exposing FractionFunction's private symbolic tree representation.

Attach a certified realization

Numerics supplies an algorithm without becoming the owner of the abstract identity:

Runnable RiXRun cell

.Plugin.Load("calculus"); .Plugin.Load("numerics"); CertifiedExp := (x) -> .numerics.Exp(x); Exp := .calculus.Exp(CertifiedExp); result := .numerics.Refine(Exp(1/2), {= absoluteWidth=1/1000, maxWork=40 }); .Table({= columns=["semantic function", "status", "certified", "interval"], rows=[[ Exp.SemanticId(), result[:status], result[:certified], result[:interval] ]] });

Propagate links through composition and differentiation

A composite Calculus graph does not copy numerical closures into its portable records. Instead, evaluation resolves every semantic application by ID. Exact differentiation builds a new graph first; surviving semantic applications then find the same linked providers:

Runnable RiXRun cell

.Plugin.Load("calculus"); .Plugin.Load("numerics"); x := .calculus.Variable(:x); Exp := .calculus.Exp((value)->.numerics.Exp(value)); Log := .calculus.Log((value)->.numerics.Ln(value)); expression := Exp(Log(x)); derivative := .calculus.DifferentiateResult(expression,:x); evaluation := .calculus.EvaluateResult(derivative,{= x=2 }); refined := .numerics.Refine(evaluation[:value],{= absoluteWidth=1/1000, maxWork=40 }); .Table({= columns=["exact derivative", "implementation IDs", "obligations", "refined value"], rows=[[ .calculus.ToSpec(derivative[:expression]), evaluation[:links].Map((link)->link[:semanticId]), evaluation[:obligationValues], refined[:interval] ]] });

Both Log and Exp are resolved during evaluation, and their implementation evidence appears in evaluation[:links]. The exact rule for Log still leaves the positive-argument obligation. Its subject is evaluated at 2, but its status remains unresolved: numerical evaluation is not a proof engine.

If an exact rule eliminates a semantic application—for example the outer Log in D Log(x)=1/x—the derivative no longer needs that implementation.

Course trigonometric and absolute-value graphs

The course CAS uses public Calculus nodes rather than private symbolic output. Sin, Cos, and Atan have exact derivative identities. Abs is portable and executable on exact reals, but has no unconditional derivative rule at zero.

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); {: .calculus.Abs()(x),.calculus.Abs()(-3), .calculus.ToSpec(.calculus.Differentiate(.calculus.Sin()(x),:x)), .calculus.ToSpec(.calculus.Differentiate(.calculus.Cos()(x),:x)), .calculus.ToSpec(.calculus.Differentiate(.calculus.Atan()(x),:x)) };

Conversely, an unknown semantic function cannot be differentiated merely because it has a numerical algorithm.

Reuse differential identities without broad algebraic rewriting

The differentiator uses exact identities already registered for a semantic function to retain a smaller evaluation graph. For a base satisfying f' = c*f, the Integer power rule can keep the base as one structural node:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); Exp := .calculus.Exp((value)->value+1); result := .calculus.DifferentiateResult(Exp(x)^2,:x); evaluation := .calculus.EvaluateResult(result,{= x=2 }); {: .calculus.ToSpec(result[:expression]), result[:evidence], evaluation[:semanticEvaluations] };

The exact derivative is represented as 2 * Exp(x)^2, and its power-rule evidence records differentialIdentityReuse. This is deliberately local: it uses D Exp = Exp, but does not invoke the separate algebraic identity Exp(a)*Exp(b) = Exp(a+b).

Linked evaluation also caches structurally identical semantic applications:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); Shift := .calculus.Function("tutorial.shift@1", {= name=:Shift, implementation=(value)->value+1, implementationEvidence=:definition }); expression := Shift(x)+Shift(x); shared := .calculus.EvaluateResult(expression,{= x=2 }); repeated := .calculus.EvaluateResult(expression,{= x=2 },{= reuseCommonSubexpressions=_ }); {: shared[:value], shared[:semanticEvaluations], shared[:reuseCount], repeated[:semanticEvaluations] };

The default result invokes Shift once and records one commonSubexpressionReuse; the opt-out invokes it twice. Sharing assumes that linked mathematical implementations are referentially transparent. Disable it for diagnostic or intentionally stateful callables.

Compute higher and multivariate derivatives

Repeated and mixed derivatives retain the variable path and accumulate prior conditions:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); y := .calculus.Variable(:y); f := x^2+x*y+y^2; gradient := .calculus.Gradient(f,[:x,:y]); jacobian := .calculus.Jacobian([x*y,x+y],[:x,:y]); hessian := .calculus.Hessian(f,[:x,:y]); higher := .calculus.DifferentiateNResult(.calculus.Log()(x),:x,2); {: gradient.Map((entry)->.calculus.ToSpec(entry)), jacobian.Map((row)->row.Map((entry)->.calculus.ToSpec(entry))), hessian.Map((row)->row.Map((entry)->.calculus.ToSpec(entry))), .calculus.ToSpec(higher[:expression]), higher[:variables], higher[:obligations] };

GradientResult, JacobianResult, and HessianResult expose every component transformation plus their flattened obligations. The shorter forms used above return expression arrays only when all components are unconditional.

Keep the three meanings of an integral distinct

Phase 3 begins with inert records rather than prematurely choosing an integration algorithm:

Runnable RiXRun cell

.Plugin.Load("calculus"); x := .calculus.Variable(:x); integrand := 2*x; primitive := x^2; selected := .calculus.SelectedPrimitive(integrand,:x,primitive,{= verification=:declaredIdentity, evidence=[:powerRule] }); family := .calculus.AntiderivativeFamily(integrand,:x,primitive,:C); definite := .calculus.DefiniteIntegral(integrand,:x,0,3); {: selected, family, definite };

A selected primitive names one representative. An antiderivative family keeps that representative and the integration-constant symbol in separate fields. A definite integral retains its lower and upper endpoints. All three use rix.calculus.integral@1 and carry explicit obligations and evidence. They do not yet claim that a primitive has been checked or that a definite integral has been evaluated; later exact and Numerics providers will consume these records without changing their mathematical meaning.

The Calculus record and registry say which mathematical function and exact rule are meant. The Numerics result says how a value was computed and what evidence the finite work supports. Integral records now extend this same boundary; exact integration, certified quadrature, and equation specifications remain later steps.

Bounded course continuation

See [the executable course calculus guide](../../documentation/eval/course-calculus.md) for mixed powers, radicals, definite integrals, local domain rewrites, and inert equation/declared-derivative records. It includes exact, bounded-failure and explicitly approximate examples.