Warning: This resource is provisional

Function Repository Resource:

FindReplacePath

Find a path that goes from one expression to another with a sequence of replacements

Contributed by: Nikolay Murzin

ResourceFunction["FindReplacePath"][theorem, axioms]

finds a replacement path from the left-hand side of a theorem to its right-hand side using replacements specified by axioms.

ResourceFunction["FindReplacePath"][theorem,axioms,prop]

return a specified property of a path.

Details and Options

ResourceFunction["FindReplacePath"] uses FindEquationalProof to find a proof of an equational proposition, and by process of cut-elimination it derives a sequential path of one-step replacements from one side of a theorem to the other.

The path consists of pattern expressions corresponding to logic formulas with patterns (like a_) representing universal variables (ForAll) and other symbols representing functional constants (Exists).

The list of ResourceFunction["FindReplacePath"] properties includes:

"ProofObject"

corresponding ProofObject

"Path"

list of expressions constituting a found path (default)

"Justification"

list of axioms used in each subsequent step of a path together with their orientations and positions

"Rewrites"

list of rewriting functions that reproduce a path

"PathTest"

test path endpoints to match a required statement

"RewritesTest"

test-rewriting functions to successfully reproduce a path

All

all of the above as an association

Examples

Basic Examples (2)

Find a replacement path given a set of equations:

In[1]:=

Out[1]=

Find a replacement path using universally quantified equations:

In[2]:=

ResourceFunction["FindReplacePath"][
ForAll[{x, y}, plus[x, plus[y, 0]] == plus[x, plus[0, y]]], {ForAll[x, plus[x, 0] == x], ForAll[x, plus[x, neg[x]] == 0], ForAll[{x, y, z}, plus[plus[x, y], z] == plus[x, plus[y, z]]]}]

Out[2]=

In[3]:=

ResourceFunction["FindReplacePath"][
ForAll[x, neg[neg[x]] == x], {ForAll[x, plus[x, 0] == x], ForAll[x, plus[x, neg[x]] == 0], ForAll[{x, y, z}, plus[plus[x, y], z] == plus[x, plus[y, z]]]}]

Out[3]=

In[4]:=

ResourceFunction["FindReplacePath"][
ForAll[{a, b}, or[not[or[not[a], b]], not[or[not[a], not[b]]]] == a], {ForAll[{a, b}, and[a, b] == and[b, a]], ForAll[{a, b}, or[a, b] == or[b, a]], ForAll[{a, b}, and[a, or[b, not[b]]] == a], ForAll[{a, b}, or[a, and[b, not[b]]] == a], ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]], ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}]

Out[4]=

In[5]:=

ResourceFunction["FindReplacePath"][
ForAll[{a, b, c, d}, g[a, inv[g[b, g[g[g[c, inv[c]], inv[g[d, b]]], a]]]] == d], {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e]}] // Short

Out[5]=

In[6]:=

ResourceFunction["FindReplacePath"][
ForAll[{a, b, c}, g[g[g[a, b], c], inv[g[a, c]]] == b], {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e], ForAll[{a, b}, g[a, b] == g[b, a]]}]

Out[6]=

Scope (5)

Use names from AxiomaticTheory:

In[7]:=

Out[7]=

Use ProofObject to find a path:

In[8]:=

Out[8]=

In[9]:=

Out[9]=

Find a path in a string substitution system:

In[10]:=

Out[10]=

In[11]:=

Out[11]=

Find a path in a Wolfram model system:

In[12]:=

Out[12]=

In[13]:=

ResourceFunction["WolframModelPlot"][#, VertexLabels -> Automatic] & /@
removeBetweenEqual@(First /@ Gather[Sort /@ (List /@ ResourceFunction["FindReplacePath"][proof, "Path"] /. {CircleMinus | CirclePlus | CircleTimes -> List,
CircleDot -> Sequence})]) // Reverse

Out[13]=

Reproduce the found path using rewriting functions:

In[14]:=

Out[14]=

In[15]:=

$FoldList[#2[#1] &, a_\[CircleTimes](a_\[CirclePlus]b_), %]$

Out[15]=

Possible Issues (1)

Degenerate axiom systems capable of deriving a==b-type statements can sometimes fail:

In[16]:=

$ResourceFunction["FindReplacePath"][a == b, ForAll[{a, b, c}, (c\[SmallCircle]a)\[SmallCircle]((b\[SmallCircle]a)\[SmallCircle]b) == a]]$

Out[16]=

In[17]:=

$ResourceFunction["FindReplacePath"][ a\[SmallCircle]((b\[SmallCircle]b)\[SmallCircle]b) == b\[SmallCircle](b\[SmallCircle](a\[SmallCircle]b)), ForAll[{a, b, c}, (c\[SmallCircle]a)\[SmallCircle]((b\[SmallCircle]a)\[SmallCircle]b) == a]]$

Out[17]=

Neat Examples (2)

Test Boolean theorems:

In[18]:=

AssociationMap[
ResourceFunction["FindReplacePath"][#, "BooleanAxioms", All][[{"PathTest", "RewriteTest"}]] & /@ AxiomaticTheory["BooleanAxioms", "NotableTheorems"][#] &, Keys@AxiomaticTheory["BooleanAxioms", "NotableTheorems"]]

Out[18]=

NKS example:

In[19]:=

$proof = FindEquationalProof[p\[CenterDot]q == q\[CenterDot]p, {\!$ \*SubscriptBox[\(\[ForAll]$, $\[FormalA]$]$\((\[FormalA]\[CenterDot]\[FormalA])$\[CenterDot]$(\[FormalA]\[CenterDot]\[FormalA])$\)\) \[Implies] \[FormalA], \!$ \*SubscriptBox[\(\[ForAll]$, ${\[FormalA], \[FormalB]}$]$\[FormalA] == \((\[FormalA]\[CenterDot]\[FormalA])$\[CenterDot]$(\[FormalA]\[CenterDot]\[FormalB])$\)\), \!$ \*SubscriptBox[\(\[ForAll]$, ${\[FormalA], \[FormalB]}$]$\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalB])$ == \[FormalA]\[CenterDot]$(\[FormalB]\[CenterDot]\[FormalB])$\)\), \!$ \*SubscriptBox[\(\[ForAll]$, ${\[FormalA], \[FormalB], \[FormalC]}$]$\((\[FormalA]\[CenterDot]\((\[FormalA]\[CenterDot]\((\[FormalB]\[CenterDot]\[FormalC])$)\))\) == $(\[FormalB]\[CenterDot]\((\[FormalB]\[CenterDot]\((\[FormalA]\[CenterDot]\[FormalC])$)\))\)\)\)}]$