Function Repository Resource:

FindFiniteModels

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 k^{k^a} 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 (7)

Find binary models for a nullary operator:

In[1]:=

Out[1]=

Find ternary models for a nullary operator:

In[2]:=

Out[2]=

Find binary models for unary operators:

In[3]:=

Out[3]=

In[4]:=

Out[4]=

In[5]:=

Out[5]=

Find binary models for a binary operator:

In[6]:=

Out[6]=

Find ternary models for a binary operator:

In[7]:=

Out[7]=

Find binary models for a ternary operator:

In[8]:=

Out[8]=

Include constants:

In[9]:=

Out[9]=

Scope (8)

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

In[10]:=

Out[10]=

Multiple operators with different arities are supported:

In[11]:=

Out[11]=

Inequalities:

In[12]:=

Out[12]=

In[13]:=

Out[13]=

In[14]:=

Out[14]=

Alternatives:

In[15]:=

Out[15]=

Disjunctions:

In[16]:=

Out[16]=

Quantifiers:

In[17]:=

Out[17]=

In[18]:=

Out[18]=

String relations have additional axioms:

In[19]:=

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

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

Out[22]=

In[23]:=

Out[24]=

Parallelize (1)

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

In[25]:=

$Length@ResourceFunction["FindFiniteModels"][ b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> False] // AbsoluteTiming$

Out[25]=

In[26]:=

$Length@ResourceFunction["FindFiniteModels"][ b\[SmallCircle](a\[SmallCircle]a) == a, 8, "Parallelize" -> True] // AbsoluteTiming$

Out[26]=

In[27]:=

$ResourceFunction[ "FindFiniteModels"][((\[FormalB]\[CenterDot]\[FormalC])\[CenterDot]\[FormalA])\[CenterDot](\[FormalB]\[CenterDot]((\[FormalB]\[CenterDot]\[FormalA])\[CenterDot]\[FormalB])) == \[FormalA], 4, "Parallelize" -> False] // AbsoluteTiming$

Out[27]=

In[28]:=

Out[28]=

MaxItems (1)

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

In[29]:=

Out[30]=

Neat Examples (3)

Define functions to be used throughout this example:

In[31]:=

$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[32]:=

$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[32]=

Reproduce and extend some NKS book examples:

In[33]:=

$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[34]:=

$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[35]:=

$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[36]:=

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

$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}]$