idp_engine.Interpret

Methods to ground / interpret a theory in a data structure

  • expand quantifiers

  • replace symbols interpreted in the structure by their interpretation

  • instantiate definitions

( see docs/zettlr/Substitute.md )

interpret_definition(self, problem)[source]

updates problem.def_constraints, by expanding the definitions

Parameters
  • problem (Theory) – containts the enumerations for the expansion; is updated with the expanded definitions

  • self (Parse.Definition) –

Return type

None

interpret_expression(self, problem, subs)[source]

expand quantifiers and replace symbols interpreted in the structure by their interpretation

Parameters
  • self (Expr.Expression) – the expression to be interpreted

  • problem (Optional[Theory]) – the theory to be applied

  • subs (dict[str, Expr.Expression]) – a dictionary mapping variable names to their value

Returns

the interpreted expression

Return type

Expression

extension(self, extensions)[source]

returns the extension of a SetName, given some interpretations.

Normally, the extension is already in extensions by SymbolDeclaration.interpret. However, for Concept[T->T], an additional filtering is applied.

Parameters
  • interpretations (dict[str, SymbolInterpretation]) –

  • symbols (the known interpretations of types and) –

  • extensions (dict[str, Expr.Extension]) –

Returns

a superset of the extension of self, and a function that, given arguments, returns an Expression that says whether the arguments are in the extension of self

Return type

Extension

get_supersets(self, problem)[source]

determine the extent of the variables, if possible, and add a filter to the quantified expression if needed. This is used to ground quantification over unary predicates.

Example

type T := {1,2,3} p : T -> Bool // p is a subset of T !x in p: q(x)

The formula is equivalent to !x in T: p(x) => q(x). -> The superset of p is {1,2,3}, the filter is p(x). The grounding is (p(1)=>q(1)) & (p(2)=>q(2)) & (p(3)=>q(3))

If p is enumerated (p:={1,2}) in a structure, however, the superset is now {1,2} and there is no need for a filter. The grounding is q(1) & q(2)

Result:

self.supersets is updated to contain the supersets self.sub_exprs are updated with the appropriate filters

Parameters
  • self (Expr.AQuantification | Expr.AAggregate) –

  • problem (Optional[Theory]) –

Return type

None