kdrag.utils.alpha_norm

kdrag.utils.alpha_norm(expr: ExprRef) → ExprRef

Recursively rename all variables in an expression to canonical names. Printed form may become ambiguous because internally de Bruijn indices are used.

>>> x,y,z,w = smt.Consts("x y z w", smt.IntSort())
>>> p = smt.Real("p")
>>> assert not smt.Lambda([x,y], x + y).eq(smt.Lambda([z,w], z + w))
>>> assert alpha_norm(smt.Lambda([x,y], x + y)).eq(alpha_norm(smt.Lambda([z,w], z + w)))
>>> _ = kd.prove(alpha_norm(smt.Lambda([x,p], p)) == smt.Lambda([x,p], p))

Parameters:

expr (ExprRef)

Return type:

ExprRef