Logic Fragments

Previous Next

Reference

Logic fragments and typed tuple-based formulas.

This module defines
  • TLExpr: a lightweight AST for temporal/propositional logic as typed tuples
  • Utilities to validate/inspect/transform formulas
  • LogicFragment meta-class to declare connectives and compose language fragments
Design
  • A proposition is either a string name or a SetBuilder constant.
  • Operator applications are tuples of the form:
    • (op,) for nullary operators
    • (op, arg) for unary operators
    • (op, lhs, rhs) for binary operators
  • Operators are declared via declare(name, narg) which produces a class-like fragment whose __call__ constructs the tuple form.
  • Fragments can be composed with | to create a combined language.

LogicFragment

Bases: type

Metaclass for declaring and composing logic fragments (connectives).

Instances of classes produced by this metaclass are not meant to be instantiated. Instead, calling the class constructs a tuple-based TLExpr for the associated connective (see call).

Attributes:

Name Type Description
- __narg__

required arity for the connective (None for a composed fragment)
- __connectives__

tuple of connective names included in this fragment
Composition
  • Fragments can be combined with | to form a new fragment whose __connectives__ is the union of the operands.

__call__(*args)

Construct a TLExpr tuple for this connective.

Constraints
  • This only works for a fragment with exactly one connective.
  • Number of arguments must match the declared arity.
  • Arguments must themselves be valid TLExpr terminals or tuples.

Returns:

Type Description
TLExpr
  • (op,) | (op, arg) | (op, lhs, rhs), where op == cls.name

__new__(mcs, name, bases, namespace)

Create a new fragment type, merging connectives from base fragments.

__or__(*args)

Return a fragment that is the union of this fragment and others.

is_complete(prims)

Check that all connectives in this fragment exist in prims.

declare(name, narg)

Declare a new connective fragment with given name and arity.

Parameters:

Name Type Description Default
- name

operator name used as the tuple head in TLExpr

 required
- narg

arity (0, 1, or 2)

 required

Returns:

Type Description
LogicFragment
  • A LogicFragment-derived class representing the connective

get_malformed(formula)

Return the first malformed subexpression, or None if well-formed.

Parameters:

Name Type Description Default
- formula

TLExpr to check

 required

Returns:

Type Description
Optional[TLExpr]
  • None if the expression is well-formed; otherwise the first offending subexpression
Well-formedness rules
  • Propositions: non-empty str, or any SetBuilder instance
  • Operator tuples: length 1..3, head must be str, and all arguments recursively valid

get_props(formula)

Collect proposition names appearing in a formula.

  • String terminals are treated as proposition names and included.
  • SetBuilder terminals are constants and contribute no proposition names.
  • Operator tuples are traversed recursively.

Parameters: - formula: TLExpr to inspect

Returns: - Set of unique proposition names found in formula

replace_prop(formula, prop, expr)

Replace all occurrences of proposition prop with expr.

Parameters:

Name Type Description Default
- formula

operator tuple (TLOpNullary/Unary/Binary)

 required
- prop

proposition name to replace

 required
- expr

replacement sub-expression

 required

Returns:

Type Description
TLExpr
  • New TLExpr with replacements applied
Notes
  • This function expects formula to be an operator tuple (not a raw str or SetBuilder). It descends recursively and replaces terminals that match prop.
  • For nullary or terminal positions, if the terminal equals prop, it is replaced by expr.
Set Builders Temporal Logic Trees