Function Repository Resource:

FindFiniteModels

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

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

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

In[10]:=

Out[10]=

Multiple operators with different arities is 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

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

Out[21]=

In[22]:=

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

Out[26]=

MaxItems

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

In[27]:=

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