prodigy.pgcl.substitute

Variable Substitution

This module does variable substitution for expressions, expectations, and programs. The purpose of this module is elimination of SubstExpr by applying the corresponding substitutions.

Note

The program must be well-typed. In particular, variables must be defined before they are used and substitutions must be type-safe.

Warning

The input AST must be a tree and objects may not occur multiple times. This is a limitation of the current implementation. General DAGs are not supported yet.

Warning

Substitutions reuse AST objects, and do not copy unnecessarily. Thus, AST objects may turn up multiple times in the AST. For later mutation of the AST, you may want to pass deepcopy = True to prevent spooky action action at a distance.

Symbolic variables

Each substitution function takes a parameter symbolic parameter that is a set of variables to be taken symbolic. Symbolic variables are placeholders for arbitrary expressions, and thus it is not known which variables they contain. Therefore the substitution cannot be done at this time. Instead, a substitution applied to a symbolic variable will wrap the variable in a SubstExpr that contains all substitutions applied to this variable.

>>> from prodigy.pgcl.util.ref import Mut
>>> from .ast import SubstExpr, NatLitExpr, VarExpr
>>> from .parser import parse_expr

Simple substitution without symbolic variables:
>>> expr_ref = Mut.alloc(SubstExpr({"x": NatLitExpr(2)}, parse_expr("x + y")))
>>> substitute_expr(expr_ref)
>>> str(expr_ref.val)
'2 + y'

The same substitution with `y` being symbolic:
>>> expr_ref = Mut.alloc(SubstExpr({"x": NatLitExpr(2)}, parse_expr("x + y")))
>>> substitute_expr(expr_ref, symbolic=set("y"))
>>> str(expr_ref.val)
'2 + ((y)[x/2])'

Implementation notes

See also

Documentation of internal classes and functions can be found on another page.

The implementation is much more sophisticated than the simple approach of doubly-recursive bottom-up substition application. For comparison, the simple approach is available in tests/test_substitution.py and used to test this implementation. In this module, we implement a different approach using generated local variables for each substitution.

First the binding phase, top-down (implemented in _Binder.bind()):

  1. For each substitution expression and each substitution x/y, generate a new local variable t.

  2. Run all current substitutions on y, generating y’.

  3. Now remember two substitutions: x/t and t/y’.

  4. Recurse into the substitutions’ children.

Then the resolve phase (direction is irrelevant, implemented in _Binder.resolve()):

  1. On the generated substitutions for local variables, replace all simple ones of the form t1/t2, resolving t2 recursively. Now the object references to be inserted in the AST are final (not necessarily nested objects).

  2. Now we update the objects to be inserted in the AST, i.e. all replacements of the form t1/r for general expressions r are updated by replacing all locals t_i occuring in r. All substitutions are now final.

  3. Replace all locals in the expression itself.

Except for step 1 of the resolve phase, all phases clearly take linear time. Step 1 of resolve is only run for simple chains of substitutions with no nested locals (e.g. generated from x[x/y][y/z]), and the step also amortizes lookups. So basically we have linear runtime.

This implementation was very loosely inspired by an article [1] on “locally nameless” substitution based on the awesomely titled paper “I am not a Number — I am a Free Variable” [2].

Footnotes

substitute_expr(expr_ref, *, symbolic=None, deepcopy=False)[source]

Apply substitutions in this expression/expectation. After execution, the expr_ref contains no SubstExpr anywhere except directly around symbolic variables.

Parameters:

  • expr_ref (Mut[VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr]) – The reference to the expression to be modified.

  • symbolic (FrozenSet[str] | None) – The set of symbolic variables. See the module description.

  • deepcopy (bool) – Whether to call deepcopy on each replacement, i.e. not reuse any AST objects in substitutions.

substitute_constants_expr(program, expr_ref, *, symbolic=None)[source]

Substitute constants in this expression/expectation.

Parameters:

  • program (Program) – The program with variable declarations.

  • expr_ref (Mut[VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr]) – The reference to the expression to be modified.

  • symbolic (FrozenSet[str] | None) – The set of symbolic variables. See the module description.

substitute_constants(program, *, symbolic=None)[source]

Substitute constants in this program.

>>> from prodigy.pgcl.parser import parse_pgcl
>>> program = parse_pgcl("const x := 23; nat y; nat z; y := x; z := y")
>>> substitute_constants(program)
>>> program.instructions
[AsgnInstr(lhs='y', rhs=NatLitExpr(23)), AsgnInstr(lhs='z', rhs=VarExpr('y'))]
Parameters:

  • program (Program) – The program to be modified.

  • symbolic (FrozenSet[str] | None) – The set of symbolic variables. See the module description.