Function Repository Resource:

FindFiniteModels

Source Notebook

Find 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 two 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/inequalities 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
"Models"returns a list of models
The following options can be given:
Method"ExpressionPrune"the method to use
"Parallelize"Falsewhether to run some operations in parallel
MaxItemsInfinitylimit the number of returned models
"ReverseOrdering"Falseordering of indices
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
Automaticsame as "ExpressionPrune"

Examples

Basic Examples (7) 

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 (8) 

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 (8) 

Method (1) 

"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 (1) 

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 (1) 

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]=

ReverseOrdering (5) 

By default, models are indexed by their corresponding inputs (shifted by 1). For example, a model of Not for BooleanAxioms is {1, 0} because {1, 0}[[0+1]] ==1 and {1, 0}[[1+1]] ==0:

In[28]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["BooleanAxioms"]]
Out[28]=

For some cases, like the default ordering of truth tables for boolean expressions, the convention is to use a reversed ordering {1,0}<->{True,False}:

In[29]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["BooleanAxioms"],
  "ReverseOrdering" -> True]
Out[29]=

For the first {8, 14, 1}, with "ReverseOrdering"True, model indices correspond exactly to BooleanFunction indices and models to truth tables. Here CirclePlus is a model of And:

In[30]:=
Boole@BooleanTable[BooleanFunction[8, 2], {1}, {2}]
Out[30]=
In[31]:=
ResourceFunction["TruthTable"]@BooleanFunction[8, 2]
Out[31]=

CircleTimes is a model of Or:

In[32]:=
Boole@BooleanTable[BooleanFunction[14, 2], {1}, {2}]
Out[32]=
In[33]:=
ResourceFunction["TruthTable"]@BooleanFunction[14, 2]
Out[33]=

OverBar is a model of Not:

In[34]:=
Boole@BooleanTable[BooleanFunction[1, 1]]
Out[34]=
In[35]:=
ResourceFunction["TruthTable"]@BooleanFunction[1, 1]
Out[35]=

Neat Examples (3) 

Define functions to be used throughout this example:

In[36]:=
NestedTupleFromIndex[index_, k_, n_] := ArrayReshape[IntegerDigits[index, k, k^n], Table[k, n]]

plotRelationConstraints // ClearAll
plotRelationConstraints[expr_, k_ : 2, limit_ : Infinity, n_ : UpTo[6]] := Module[{indices = ResourceFunction["FindFiniteModels"][expr, k, "Indices", "Parallelize" -> True, MaxItems -> limit], sampleIndices, tables},
  sampleIndices = Take[indices, n];
  tables = Map[NestedTupleFromIndex[#[[1]], k, 2] &, sampleIndices];
  Framed@Row[
    Append[
     ArrayPlot[#, Mesh -> True, ImageSize -> 32] & /@ tables, If[Length[sampleIndices] == 0, Row@{"(", 0, ")"}, If[Length[indices] - Length[sampleIndices] > 0, Row@{"\[Ellipsis]", "(", Length[indices], ")"}, Nothing]]
     ]
    ]
  ]

Find models for abelian semigroup theory axioms:

In[37]:=
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[37]=

Reproduce and extend some :

In[38]:=
Scan[relation |-> 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[39]:=
Scan[relation |-> 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[40]:=
Scan[relation |-> 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[41]:=
Scan[relation |-> Print[AbsoluteTiming@
    Row[Riffle[
      Prepend[plotRelationConstraints[{relation}, #] & /@ Range[2, 3],
        Framed[relation, Background -> LightGray]], Spacer[8]]]], {b\[SmallCircle](a\[SmallCircle]a) == 0}]
In[42]:=
Scan[relation |-> 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[43]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 2]
Out[43]=
In[44]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 3]
Out[44]=
In[45]:=
ResourceFunction[
 "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> True]
Out[45]=

AxiomaticTheory examples:

In[46]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 2]
Out[46]=
In[47]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 3]
Out[47]=
In[48]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["GroupAxioms"] /. OverTilde[x_] :> x[], 4, MaxItems -> 1]
Out[48]=
In[49]:=
ResourceFunction["FindFiniteModels"][
 AxiomaticTheory["RingAxioms"] /. OverTilde[x_] :> x[]]
Out[49]=
In[50]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["BooleanAxioms"]]
Out[50]=
In[51]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["WolframAxioms"]]
Out[51]=
In[52]:=
ResourceFunction["FindFiniteModels"][AxiomaticTheory["HillmanAxioms"]]
Out[52]=

Publisher

N. Murzin

Version History

  • 1.1.0 – 07 February 2024
  • 1.0.0 – 16 September 2020

Related Resources

License Information