Wolfram Research

Function Repository Resource:

FindFiniteModels

Source Notebook

Finds finite models consistent with the set of relations

Contributed by: Nikolay Murzin

ResourceFunction["FindFiniteModels"][rels]

finds models in form of multiplication tables consistent with the relations rels for each operator in rels, assuming each variable can have one of 2 values.

ResourceFunction["FindFiniteModels"][rels,k]

allows k≥2 values for each variable.

ResourceFunction["FindFiniteModels"][rels,k,prop]

returns a specified property prop of found models.

Details and Options

The relations rels can be given in terms of operators in logical form with equalities/unequalities or string relations.
There are kka models for each operator of arity a.
Property prop may be one of following:
"Association" returns an association with multiplication tables as values and indices as keys for each found model (default)
"Indices" returns a list of indices for models
The following options can be given:
Method "ExpressionPrune" the method to use
"Parallelize" False whether to run some operations in parallel
MaxItems Infinity limit the number of returned models
The following values can be given for the Method option:
"ExpressionPrune" pruned search over relations converted to a conjunction of DNFs
"BruteForce" a complete search over all possible models
Automatic same as “ExpressionPrune”

Examples

Basic Examples

Find binary models for a nullary operator:

In[1]:=
ResourceFunction["FindFiniteModels"][a[] -> a[]]
Out[1]=

Find ternary models for a nullary operator:

In[2]:=
ResourceFunction["FindFiniteModels"][a[] == b[], 3]
Out[2]=

Find binary models for unary operators:

In[3]:=
ResourceFunction["FindFiniteModels"][f[a] == a]
Out[3]=
In[4]:=
ResourceFunction["FindFiniteModels"][f[a] == b]
Out[4]=
In[5]:=
ResourceFunction["FindFiniteModels"][f[a] == g[a], 2]
Out[5]=

Find binary models for a binary operator:

In[6]:=
ResourceFunction["FindFiniteModels"][f[a, b] == a]
Out[6]=

Find ternary models for a binary operator:

In[7]:=
ResourceFunction["FindFiniteModels"][f[a, b] == f[b, a], 3]
Out[7]=

Find binary models for a ternary operator:

In[8]:=
ResourceFunction["FindFiniteModels"][f[a, b, c] == f[a, b, b]]
Out[8]=

Include constants:

In[9]:=
ResourceFunction["FindFiniteModels"][f[a, b] == g[0] == 1]
Out[9]=

Scope

In absence of operators FindFiniteModels assumes all atoms are nullary operators:

In[10]:=
ResourceFunction["FindFiniteModels"][a -> b]
Out[10]=

Multiple operators with different arities is supported:

In[11]:=
ResourceFunction["FindFiniteModels"][f[a, b] == g[b, f[b, a], a]]
Out[11]=

Inequalities:

In[12]:=
ResourceFunction["FindFiniteModels"][a != b]
Out[12]=
In[13]:=
ResourceFunction["FindFiniteModels"][f[a, b] != 0]
Out[13]=
In[14]:=
ResourceFunction["FindFiniteModels"][f[b, f[a, a]] != b]
Out[14]=

Alternatives:

In[15]:=
ResourceFunction["FindFiniteModels"][f[a, b] != a | f[a, b] == a]
Out[15]=

Disjunctions:

In[16]:=
ResourceFunction["FindFiniteModels"][f[a, b] != a || f[a, b] == a]
Out[16]=

Quantifiers:

In[17]:=
ResourceFunction["FindFiniteModels"][Exists[{x}, x == f[x, y]]]
Out[17]=
In[18]:=
ResourceFunction["FindFiniteModels"][ForAll[{f, x}, x == f[x, y]]]
Out[18]=

String relations have additional axioms:

In[19]:=
ResourceFunction["FindFiniteModels"]["ABBA" -> "BAAB"]
Out[19]=

String relations form a monoid with binary associative operator ∘ (\[SmallCircle]) and nullary identity 1:

In[20]:=
ResourceFunction["FindFiniteModels"]["A" -> "AA", 3] == ResourceFunction[
  "FindFiniteModels"][{"A" == "A"\[SmallCircle]"A", ("A"\[SmallCircle]"B")\[SmallCircle]"C" == "A"\[SmallCircle]("B"\[SmallCircle]"C"), "1"[]\[SmallCircle]"A" == "A", "A"\[SmallCircle]"1"[] == "A"}, 3]
Out[20]=

Options

Method

"BruteForce" method may be useful if a relation is very general so that enumerating models and finding a small subset of them returns faster:

In[21]:=
ResourceFunction["FindFiniteModels"][f[0, a] == 0, 4, MaxItems -> 2] // AbsoluteTiming
Out[21]=
In[22]:=
ResourceFunction["FindFiniteModels"][f[0, a] == 0, 4, MaxItems -> 2, Method -> "BruteForce"] // AbsoluteTiming
Out[22]=

Parallelize

Setting the option "Parallelize" to True may speed up computation:

In[23]:=
Length@ResourceFunction["FindFiniteModels"][
   b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> False] // AbsoluteTiming
Out[23]=
In[24]:=
Length@ResourceFunction["FindFiniteModels"][
   b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> True] // AbsoluteTiming
Out[24]=
In[25]:=
ResourceFunction[
  "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\
\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\
\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> False] // AbsoluteTiming
Out[25]=
In[26]:=
ResourceFunction[
  "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\
\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\
\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> True] // AbsoluteTiming
Out[26]=

MaxItems

Limiting a number of returned models reduces an amount of performed computation:

In[27]:=
ResourceFunction["FindFiniteModels"][f[b, f[a, b]] == a, 10, MaxItems -> 2]
Out[27]=

Neat Examples

Find models for abelian semigroup theory axioms:

In[28]:=
Row[Riffle[
  plotRelationConstraints[{a\[CenterDot]b == b\[CenterDot]a, (a\[CenterDot]b)\[CenterDot]c == a\[CenterDot](b\[CenterDot]c)}, #] & /@ Range[2, 4], Spacer[8]]]
Out[28]=

Reproduce and extend some :

In[29]:=
Scan[relation \[Function] Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 4],
        Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a, b\[SmallCircle](b\[SmallCircle]a) == a}]
In[30]:=
Scan[relation \[Function] Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 6],
        Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a}]
In[31]:=
Scan[relation \[Function] Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #, 2] & /@ Range[2, 10], Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == a, b\[SmallCircle](a\[SmallCircle]b) == a}]
In[32]:=
Scan[relation \[Function] Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 3],
        Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == 0}]
In[33]:=
Scan[relation \[Function] Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 10], Framed[relation, Background -> LightGray]], Spacer[8]]]], {a\[SmallCircle]b == a, b\[SmallCircle]a == a}]

Find models for the Wolfram axiom:

In[34]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\
\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\
\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 2]
Out[34]=
In[35]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\
\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\
\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 3]
Out[35]=
In[36]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\
\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\
\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> True]
Out[36]=

AxiomaticTheory examples:

In[37]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 2]
Out[37]=
In[38]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 3]
Out[38]=
In[39]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 4, MaxItems -> 1]
Out[39]=
In[40]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["RingAxioms"] /. OverTilde[x_] :> x[]]
Out[40]=
In[41]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["BooleanAxioms"]]
Out[41]=
In[42]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["WolframAxioms"]]
Out[42]=
In[43]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["HillmanAxioms"]]
Out[43]=

Resource History

Related Resources

License Information