Skip to content

Generators

Generators can be used to create universally quantified variables in a way that preserves type safety.

Example:

TreeNodeType = str

class AncestorOf(BaseModel, Fact):
    ancestor: TreeNodeType
    descendant: TreeNodeType

@axiom
def ancestor_transitivity_axiom() -> bool:
    '''For all x,y,z, if AncestorOf(x,z) and AncestorOf(z,y), then AncestorOf(x,y)'''
    return all(
        AncestorOf(ancestor=x, descendant=y)
        for x, y, z in gen3(TreeNodeType, TreeNodeType, TreeNodeType)
        if AncestorOf(ancestor=x, descendant=z) and AncestorOf(ancestor=z, descendant=y)
    )

The above axiom defines a universally quantified statement over the variables x, y, and z, whose range is all strings.

Note that while the semantics of the above program are consistent with Python semantics, actually executing the above code would take infinite time as there are infinite strings. Instead, the python is treated as a logical specification.

gen(*types)

A generator that yields tuples of values of the specified types.

Note: this is more weakly typed than the arity-specific :ref:gen1, :ref:gen2, and :ref:gen3 functions.

.. note:: These are generally used in defining axioms using python syntax, rather than executed directly.

Parameters:

Name Type Description Default
types Type[Any]
()

Returns:

Type Description
Generator[Tuple[Any, ...], None, None]
Source code in src/typedlogic/generators.py 
41
42
43
44
45
46
47
48
49
50
51
52
53
def gen(*types: Type[Any]) -> Generator[Tuple[Any, ...], None, None]:
    """
    A generator that yields tuples of values of the specified types.

    Note: this is more weakly typed than the arity-specific :ref:`gen1`, :ref:`gen2`, and :ref:`gen3` functions.

    .. note:: These are generally used in defining axioms using python syntax, rather than executed directly.

    :param types:
    :return:
    """
    while True:
        yield tuple(t() for t in types)  # Replace with actual logic

gen1(type1)

A generator that yields individual values of the specified type.

.. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

Parameters:

Name Type Description Default
type1 Type[T1]
required

Returns:

Type Description
Generator[T1, None, None]
Source code in src/typedlogic/generators.py 
56
57
58
59
60
61
62
63
64
65
66
def gen1(type1: Type[T1]) -> Generator[T1, None, None]:
    """
    A generator that yields individual values of the specified type.

    .. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

    :param type1:
    :return:
    """
    while True:
        yield type1()  # R

gen2(type1, type2)

A generator that yields arity 2 tuples of values of the specified types.

.. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

Parameters:

Name Type Description Default
type1 Type[T1]
required
type2 Type[T2]
required

Returns:

Type Description
Generator[Tuple[T1, T2], None, None]
Source code in src/typedlogic/generators.py 
69
70
71
72
73
74
75
76
77
78
79
80
def gen2(type1: Type[T1], type2: Type[T2]) -> Generator[Tuple[T1, T2], None, None]:
    """
    A generator that yields arity 2 tuples of values of the specified types.

    .. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

    :param type1:
    :param type2:
    :return:
    """
    while True:
        yield type1(), type2()  # Replace with actual logic

gen3(type1, type2, type3)

A generator that yields arity 3 tuples of values of the specified types.

.. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

Parameters:

Name Type Description Default
type1 Type[T1]
required
type2 Type[T2]
required
type3 Type[T3]
required

Returns:

Type Description
Generator[Tuple[T1, T2, T3], None, None]
Source code in src/typedlogic/generators.py 
83
84
85
86
87
88
89
90
91
92
93
94
95
def gen3(type1: Type[T1], type2: Type[T2], type3: Type[T3]) -> Generator[Tuple[T1, T2, T3], None, None]:
    """
    A generator that yields arity 3 tuples of values of the specified types.

    .. note:: This is generally used in defining axioms using python syntax, rather than executed directly.

    :param type1:
    :param type2:
    :param type3:
    :return:
    """
    while True:
        yield type1(), type2(), type3()  # Replace with actual logic