Syntax¶

The fosf.syntax module handles the internal representation of fuzzy OSF logic objects, including tags, features, sorts, constraints, clauses, terms, theories and fuzzy taxonomies.

Base OSF syntax¶

class fosf.syntax.base.Tag[source]¶

Bases: str

Represent a tag symbol in an OSF term or OSF clause.

Tag is a string subclass used to distinguish tags from regular strings. It is hashable and comparable. Equality is based on both the type and the string value.

class fosf.syntax.base.Feature[source]¶

Bases: str

Represent a feature symbol in an OSF term or OSF clause.

Feature is a string subclass used to distinguish features from regular strings. It is hashable and comparable. Equality is based on both the type and the string value.

class fosf.syntax.base.Sort(value)[source]¶

Bases: object

Represent a single sort, a named element of a sort taxonomy.

Sort objects are hashable and comparable. Equality is based on both the type and the string value.

Parameters:: value (str or Sort) – The name of the sort, or an existing Sort instance. If initialized from another Sort, the .value attribute is used. Disjunctive sorts (e.g., DisjunctiveSort, FrozenDisjunctiveSort) are not allowed.
Variables:: value (str) – The name of the sort.
Raises:: TypeError – If value is not a string or a Sort instance.

class fosf.syntax.base.DisjunctiveSort(*sorts)[source]¶

Bases: Sort

Represent a mutable disjunctive sort.

A DisjunctiveSort is set of individual Sort objects and represents their union. It is mutable: sorts can be added after construction. A frozen variant can be obtained via the freeze() method.

Parameters:: *sorts (str or Sort) – One or more sorts to initialize the disjunction.
Variables:: value (set[Sort])

add(*sorts)[source]¶

Add one or more sorts to the disjunction

Parameters:: sorts (str | Sort)

freeze()[source]¶

Return an immutable FrozenDisjunctiveSort containing the same sorts.

Return type:: FrozenDisjunctiveSort

class fosf.syntax.base.FrozenDisjunctiveSort(*sorts)[source]¶

Bases: Sort

Represent an immutable disjunctive sort.

A FrozenDisjunctiveSort contains a fixed set of Sort objects representing their union. Unlike DisjunctiveSort, this class is immutable and hashable. The mutable variant can be obtained via the thaw() method.

Parameters:: *sorts (str or Sort) – One or more sorts to initialize the frozen disjunction.
Variables:: value (frozenset[Sort])

thaw()[source]¶

Return a mutable DisjunctiveSort containing the same sorts.

Return type:: DisjunctiveSort

Taxonomies¶

class fosf.syntax.taxonomy.BaseTaxonomy(edges)[source]¶

Bases: Generic[T, R]

Generic taxonomy over directed acyclic graphs with bitvector encoding.

BaseTaxonomy represents a partially ordered set of nodes using a directed acyclic graph (DAG) structure. Each node is encoded as a bitvector for efficient computation of greatest lower bounds (GLBs) and subsort relationships. Optional weights can be associated with edges. Special top and bottom elements are automatically added if missing from the input edges.

This class is generic in the node type T and the return type R for GLB computations when multiple maximal lower bounds exist.

Parameters:

Variables:

graph (nx.DiGraph) – The DAG representation of the taxonomy.
bot (T) – The bottom node in the taxonomy.
top (T) – The top node in the taxonomy.
topo (list[T]) – The list of nodes in topological order.
rank (dict[T, int]) – A mapping from nodes to their rank in the topological order.
node_to_code (dict[T, int]) – A mapping from nodes to their bitcode.
code_to_node (dict[int, T]) – A mapping from bitcodes to nodes.

Raises:

fosf.exceptions.NotADag – If the input edges form a cycle.

property top_code: int¶: The bit code of the top element

property bot_code: int¶: The bit code of the bottom element

glb(*nodes)[source]¶

Return the greatest lower bound of the input nodes:

Parameters:: nodes (T | str)
Return type:: T | R

code(node)[source]¶

Return the code associated to a node or set of nodes.

Parameters:: node (T | str | Iterable[T]) – The node or nodes for which to return a code. If an iterable of nodes is passed, the code is the bitwise OR of the codes of each node in the iterable.
Return type:: int

is_subsort(s, t)[source]¶

Check if a node is subsumed by another sort.

Parameters:

s (T | str)
t (T | str)

Return type:

bool

lower_bounds(s)[source]¶

Return the set of lower bounds of a node.

Parameters:: s (str | T)
Return type:: set[T]

class fosf.syntax.taxonomy.TagTaxonomy(edges)[source]¶

Bases: BaseTaxonomy[Tag, set[Tag]]

Taxonomy of tag symbols.

Used in fosf.syntax.theory.OsfTheory to store the ordering of Tags induced by an OSF theory.

Parameters:

edges (Iterable[tuple[str | Tag, str | Tag]]) – An iterable of edges defining the DAG. Nodes can be strings or Tag’s.

Variables:

graph (nx.DiGraph) – The DAG representation of the Tag taxonomy.
bot (Tag) – The bottom Tag in the taxonomy.
top (Tag) – The top Tag in the taxonomy.
topo (list[Tag]) – The list of tags in topological order.
rank (dict[Tag, int]) – A mapping from tags to their rank in the topological order.
node_to_code (dict[Tag, int]) – A mapping from tags to their bitcode.
code_to_node (dict[int, Tag]) – A mapping from bitcodes to tags.

class fosf.syntax.taxonomy.SortTaxonomy(edges, instances=None)[source]¶

Bases: BaseTaxonomy[Sort, DisjunctiveSort]

Taxonomy of sort symbols.

Parameters:

edges (Iterable[tuple[str | Sort, str | Sort] | tuple[str | Sort, str | Sort, float]]) – An iterable of edges defining the DAG. Each edge can optionally include a weight (float). Nodes can be strings or instances of Sort.
instances (dict[str, dict[Sort, float]] | None) – Optional dict mapping instances to the sorts they are direct members of, together with their membership degree

Variables:

graph (nx.DiGraph) – The DAG representation of the sort taxonomy.
bot (Sort) – The bottom sort in the taxonomy.
top (Sort) – The top sort in the taxonomy.
topo (list[Sort]) – The list of sorts in topological order.
rank (dict[Sort, int]) – A mapping from sorts to their rank in the topological order.
node_to_code (dict[Sort, int]) – A mapping from sorts to their bitcode.
code_to_node (dict[int, Sort]) – A mapping from bitcodes to sorts.

Raises:

fosf.exceptions.NotADag – If the input edges form a cycle.

is_subsort(s, t, any_subsort=True)[source]¶

Check if a sort is subsumed by another sort.

Parameters:

s (Sort | str) – A Sort (possibly a DisjunctiveSort)
t (Sort | str) – A Sort (possibly a DisjunctiveSort)
any_subsort (bool, default=True) – If True, if s is a DisjunctiveSort, the method checks whether any sort in s is a subsort of t

Return type:

bool

add_instance(instance, sort)[source]¶

Add an instance to a sort.

Parameters:

instance (str)
sort (str | Sort)

is_instance(instance, sort)[source]¶

Check whether an instance is a member of a sort.

Parameters:

instance (str)
sort (Sort)

glb(*nodes)[source]¶

Return the greatest lower bound of the input sorts:

Parameters:: nodes (Sort | str)
Return type:: Sort | DisjunctiveSort

class fosf.syntax.taxonomy.FuzzySortTaxonomy(edges, instances=None)[source]¶

Bases: SortTaxonomy

Parameters:

edges (Iterable[tuple[str | Sort, str | Sort] | tuple[str | Sort, str | Sort, float]]) – An iterable of edges defining the DAG. Each edge can optionally include a weight (float). Nodes can be strings or instances of Sort.
instances (dict[str, dict[Sort, float]] | None) – Optional dict mapping instances to the sorts they are direct members of, together with their membership degree

Variables:

graph (nx.DiGraph) – The DAG representation of the sort taxonomy.
bot (Sort) – The bottom sort in the taxonomy.
top (Sort) – The top sort in the taxonomy.
topo (list[Sort]) – The list of sorts in topological order.
rank (dict[Sort, int]) – A mapping from sorts to their rank in the topological order.
node_to_code (dict[Sort, int]) – A mapping from sorts to their bitcode.
code_to_node (dict[int, Sort]) – A mapping from bitcodes to sorts.

Raises:

fosf.exceptions.NotADag – If the input edges form a cycle.

add_instance(instance, sort, degree=1.0, check=True)[source]¶

Add an instance to a sort with a membership degree.

Parameters:

instance (str)
sort (str | Sort)
degree (float, default=1.0) – The membership degree.
check (bool, default=True) – If true, check that the membership degree respects the semantics of fuzzy OSF logic.

membership_degree(instance, sort)[source]¶

Compute the degree of membership of an instance to a sort or sorts.

Parameters:

instance (str)
sort (str | Sort | Iterable)

Return type:

float

degree(s: Sort | str, t: Sort | str) → float[source]¶

degree(s: Sort | str, t: Iterable[Sort | str]) → dict[Sort, float]

degree(s: Iterable[Sort | str], t: Sort | str | Iterable[Sort | str]) → dict[Sort, dict[Sort, float]]

Compute the subsumption degree of one or more sorts with repect to one or more sorts.

Parameters:

s (Sort | str | Iterable[Sort | str])
t (Sort | str | Iterable[Sort | str])

Terms¶

class fosf.syntax.terms.Term(X, s=None, subterms=None)[source]¶

Bases: object

Represent an OSF term X:s(f1 -> t1, …, fn -> tn).

Parameters:

X (Tag) – The root tag of the term.
s (Sort | None) – The root sort of the term. If None, when the OSF term is processes, it is assumed to be the top sort in a given Sort taxonomy.
subterms (dict[Feature, list[Term]] | None) – The subterms of the OSF term. In a non-normal OSF term, the same feature may point to different subterms.

Variables:

X (Tag) – The root tag of the term.
s (Sort) – The root sort of the term.
subterms (dict[Feature, list[Term]]) – Possibly empty dict mapping each feature to a list of subterms.

dfs()[source]¶: Generate subterms depth-first.

bfs()[source]¶: Generate subterms breadth-first.

to_clause()[source]¶

Transform the OSF term into an equivalent rooted clause.

Returns:: The rooted clause corresponding to the OSF term.
Return type:: RootedClause

generate_constraints()[source]¶: Generate the OSF constraints expressed by the OSF term.

tags()[source]¶

Return the set of Tag’s appearing in the OSF term.

Return type:: set[Tag]

sorts()[source]¶

Return the set of Sort’s appearing in the OSF term.

Return type:: set[Sort]

pretty_print(spaces=0, feature='')[source]¶: Pretty-print the OSF Term.

iter_subterms()[source]¶: Generate (feature, subterm) pairs.

tag_to_sort()[source]¶

Return a mapping from each Tag to its set of Sort’s.

Return type:: dict[Tag, set[Sort]]

class fosf.syntax.terms.NormalTerm(X, s=None, subterms=None)[source]¶

Bases: Term

Represent an OSF term in normal form.

Parameters:

X (Tag) – The root tag.
s (Sort | None) – The root sort. If None, when the OSF term is processes, it is assumed to be the top sort in a given Sort taxonomy.
subterms (dict[Feature, NormalTerm] | None) – The subterms of the OSF term. In a normal OSF term, each feature may point to at most one (normal) subterm.

Variables:

X (Tag) – The root tag of the term.
s (Sort) – The root sort of the term.
subterms (dict[Feature, Term]) – Possibly empty dict mapping each feature to a unique subterm.

to_clause()[source]¶

Transform the OSF term into an equivalent rooted solved clause.

Returns:: The rooted solved clause corresponding to the OSF term.
Return type:: RootedSolvedClause

equivalent_to(other)[source]¶

Return whether this Term is equivalent to another normal term.

Parameters:: other (NormalTerm)
Return type:: bool

iter_subterms()[source]¶: Generate (feature, subterm) pairs.

tag_to_sort()[source]¶

Return a mapping from each Tag to its Sort.

Return type:: dict[Tag, Sort]

Constraints¶

class fosf.syntax.constraints.Constraint[source]¶

Bases: ABC

Abstract base class for an OSF constraint.

Variables:: tags (set[Tag]) – The set of tags appearing in the constraint.

class fosf.syntax.constraints.SortConstraint(X, s)[source]¶

Bases: Constraint

Represent a sort constraint X : s.

Parameters:

s (Sort)
X (Tag)

Variables:

tags (set[Tag]) – The set of tags appearing in the constraint.

class fosf.syntax.constraints.FeatureConstraint(X, f, Y)[source]¶

Bases: Constraint

Represent a feature constraint X.f = Y.

Parameters:

X (Tag)
f (Feature)
Y (Tag)

Variables:

tags (set[Tag]) – The set of tags appearing in the constraint.

class fosf.syntax.constraints.EqualityConstraint(X, Y)[source]¶

Bases: Constraint

Represent an equality constraint X = Y.

Parameters:

X (Tag)
Y (Tag)

Variables:

tags (set[Tag]) – The set of tags appearing in the constraint.

class fosf.syntax.constraints.Clause(*constraints)[source]¶

Bases: object

Represent an OSF clause, a conjunctive set of OSF constraints.

Parameters:

*constraints (Constraint) – The initial constraints of the clause.

Variables:

constraints (set[Constraint]) – The constraints of the clause.
tags (set[Tag]) – The set of tags appearing in the constraint.
tag_to_feats (dict[Tag, dict[Feature, set[Tag]]]) – A mapping from tags to a feature->tags map.

add(*constraints)[source]¶

Add constraints to the clause.

Parameters:: constraints (Constraint)

sorts()[source]¶

Return the sorts appearing in the clause.

Return type:: set[Sort]

subclause(root)[source]¶

Return the subclause rooted at root.

Parameters:: root (Tag)
Return type:: RootedClause

normalize(taxonomy)[source]¶

Compute the normal (or solved) form of the clause.

Parameters:: taxonomy (SortTaxonomy)
Return type:: SolvedClause

rename(base_tag='X', start=0)[source]¶

Rename the tags of the clause.

Parameters:

base_tag (str, default="X") – The base name of the tags used for the renaming.
start (int, default = 0) – The base index for the tags used for the renaming. E.g., if base_tag is “X”, the tags will be X0, X1, X2, …

Return type:

Clause

class fosf.syntax.constraints.RootedClause(root, *constraints, ensure_rooted=False)[source]¶

Bases: Clause

Represent a rooted OSF clause, a clause with a distinguished root tag.

Parameters:

root (Tag) – The root of the clause.
*constraints (Constraint) – The initial constraints of the clause.
ensure_rooted (bool, default=False) – If True, ensure that the added constraints are indeed rooted.

Variables:

root (Tag) – The root Tag of the clause.
constraints (set[Constraint]) – The constraints of the clause.
tags (set[Tag]) – The set of tags appearing in the constraint.
tag_to_feats (dict[Tag, dict[Feature, set[Tag]]]) – A mapping from tags to a feature->tags map.

add(*constraints, ensure_rooted=False)[source]¶

Add constraints to the clause.

Parameters:

*constraints (Constraint) – The constraints to be added
ensure_rooted (bool, default=False) – If True, ensure that the constraints keep the clause rooted.

Raises:

RuntimeError – If ensure_rooted is True, and the added constraints do not maintain the clause rooted.

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedClause

normalize(taxonomy)[source]¶

Compute the normal (or solved) form of the clause.

Parameters:: taxonomy (SortTaxonomy)
Return type:: RootedSolvedClause

rename(base_tag='X', start=0)[source]¶

Rename the tags of the clause.

Parameters:

base_tag (str, default="X") – The base name of the tags used for the renaming.
start (int, default = 0) – The base index for the tags used for the renaming. E.g., if base_tag is “X”, the tags will be X0, X1, X2, …

Return type:

RootedClause

class fosf.syntax.constraints.SolvedClause(*constraints)[source]¶

Bases: Clause

Represent an OSF clause in solved form.

Parameters:

*constraints (Constraint) – The initial constraints of the clause.

Variables:

constraints (set[Constraint]) – The constraints of the clause.
tags (set[Tag]) – The set of tags appearing in the constraint.
tag_to_feats (dict[Tag, dict[Feature, Tag]]) – A mapping from tags to a feature->tag map.
tag_to_sort (dict[Tag, Sort]) – A mapping from each tag to its unique sort.

add(*constraints)[source]¶

Add constraints to the clause.

Parameters:: *constraints (Constraint) – The constraints to be added
Raises:: RuntimeError – If the added constraints do not maintain the clause solved.

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedSolvedClause

normalize(_)[source]¶

Compute the normal (or solved) form of the clause.

Parameters:: _ (SortTaxonomy)
Return type:: SolvedClause

class fosf.syntax.constraints.RootedSolvedClause(root, *constraints)[source]¶

Bases: SolvedClause, RootedClause

Represent a solved OSF clause with a distinguished Tag as its root.

Parameters:

root (Tag) – The root of the clause.
*constraints (Constraint) – The initial constraints of the clause.

Variables:

constraints (set[Constraint]) – The constraints of the clause.
tags (set[Tag]) – The set of tags appearing in the constraint.
tag_to_feats (dict[Tag, dict[Feature, Tag]]) – A mapping from tags to a feature->tag map.
tag_to_sort (dict[Tag, Sort]) – A mapping from each tag to its unique sort.

subclause(root)[source]¶

Return the subclause rooted at root.

Return type:: RootedSolvedClause

to_term()[source]¶

Return an equivalent NormalTerm.

Return type:: NormalTerm

equivalent_to(other)[source]¶

Return whether this clause is equivalent to another rooted solved clause.

Parameters:: other (RootedSolvedClause)
Return type:: bool

rename(base_tag='X', start=0)[source]¶

Rename the tags of the clause.

Parameters:

base_tag (str, default="X") – The base name of the tags used for the renaming.
start (int, default = 0) – The base index for the tags used for the renaming. E.g., if base_tag is “X”, the tags will be X0, X1, X2, …

Return type:

RootedSolvedClause

Theory¶

class fosf.syntax.theory.TheoryTag(tag, sort, features=None)[source]¶

Bases: object

Represent a Tag used in an OSF theory.

Parameters:

tag (Tag) – The theory tag.
sort (Sort) – The unique sort associated to this tag.
features (dict[Feature, Tag] | None) – The features defined for this tag in the OSF theory.

Variables:

tag (Tag)
sort (Sort)
features (dict[Feature, Tag]) – A possibly empty dict mapping each feature defined in the theory for this TheoryTag to the corresponding Tag.

class fosf.syntax.theory.OsfTheory(taxonomy, definitions, tags=None, ensure_closed=False)[source]¶

Bases: object

Represent an OSF theory of sort definitition.

A sort definition imposes structural constraints on OSF terms.

Parameters:

taxonomy (SortTaxonomy) – The sort taxonomy for this theory
definitions (dict[Sort, NormalTerm]) – A mapping from each Sort to its definition as a NormalTerm
tags (dict[Tag, TheoryTag] | None, default=None) – A mapping from each Tag to its TheoryTag object. If None, it is computed.
ensure_closed (bool, default=False) – If True, close the OSF theory to ensure its order-consistency.

Variables:

taxonomy (SortTaxonomy) – The background sort subsumption taxonomy.
definitions (dict[Sort, NormalTerm]) – A mapping from each Sort to its definition as a NormalTerm
tags (dict[Tag, TheoryTag]) – A mapping from each Tag to its TheoryTag object.
tag_taxonomy (TagTaxonomy) – The tag taxonomy representing the ordering on theory tags induced by the sort taxonomy and the theory.

sort(X)[source]¶

Return the sort associated to a tag in the theory.

Parameters:: X (Tag)
Return type:: Sort

features(X)[source]¶

Return the features defined for a tag in the theory.

Parameters:: X (Tag)
Return type:: dict[Feature, Tag]