Wolfram Research

Function Repository Resource:

FindCombinatorProof

Source Notebook

Attempt to find a proof of a theorem in combinatory logic using a given combinatory calculus

Contributed by: Jonathan Gorard

ResourceFunction["FindCombinatorProof"][thm,<|"Combinators"comb,"Rules"rules|>]

tries to find an equational proof of the combinatory logic theorem thm using the combinators comb and reduction rules rules.

ResourceFunction["FindCombinatorProof"][thm,calc]

tries to find an equational proof of the combinatory logic theorem thm using the named combinatory calculus calc.

Details and Options

If ResourceFunction["FindCombinatorProof"][thm,calc] succeeds in deriving the theorem thm from the combinatory calculus calc, then it returns a ProofObject expression. If it succeeds in showing that the theorem cannot be derived from the combinatory calculus, it returns a Failure object. Otherwise, it may not terminate unless time constrained.
ResourceFunction["FindCombinatorProof"] accepts both standard (named) combinatory calculi and arbitrary calculi specified via combinator reduction rules.
ResourceFunction["FindCombinatorProof"] accepts both individual theorems and lists of theorems.
ResourceFunction["FindCombinatorProof"] has the following options:
TimeConstraint Infinity how much time to allow
If ResourceFunction["FindCombinatorProof"] exceeds the specified time constraint, it returns a Failure object.
ResourceFunction["FindCombinatorProof"][thm,calc] uses the Knuth-Bendix completion algorithm to prove that the theorem thm follows from the reduction rules of the combinatory calculus calc.

Examples

Basic Examples (3) 

Prove an elementary theorem about the single-variable fixed-point (y) combinator, with the reduction rule explicitly specified:

In[1]:=
proof = ResourceFunction["FindCombinatorProof"][
  y[f] == f[f[f[f[y[f]]]]], <|"Combinators" -> {y}, "Rules" -> {y[f] == f[y[f]]}|>]
Out[1]=

Show the abstract proof network, with tooltips showing the intermediate expressions:

In[2]:=
proof["ProofGraph"]
Out[2]=

Show the complete list of proof steps as a Dataset object:

In[3]:=
proof["ProofDataset"]
Out[3]=

Typeset a natural language argument:

In[4]:=
proof["ProofNotebook"]
Out[4]=

Prove a more sophisticated theorem involving the S-K combinatory calculus:

In[5]:=
proof = ResourceFunction["FindCombinatorProof"][
  s[s[s[s]]][s][s][k] == s[k[s[s][s[s[s]]][k]]][
    k[k[s[s][s[s[s]]][k]]][
     s[s][k[s[k][s[s[s]][k]]]][k[k[s[k][s[s[s]][k]]]]]]], <|
   "Combinators" -> {s, k}, "Rules" -> {s[x][y][z] == x[z][y[z]], k[x][y] == x}|>]
Out[5]=

Show the abstract proof network:

In[6]:=
proof["ProofGraph"]
Out[6]=

Prove a theorem using one of FindCombinatorProof's built-in combinatory calculi (Schönfinkel's B-C-I calculus):

In[7]:=
proof = ResourceFunction[
  "FindCombinatorProof"][\[FormalC][\[FormalI]][\[FormalB][\[FormalX]][\[FormalI]][\[FormalZ]]][\[FormalY]] == \[FormalY][\[FormalX][\[FormalZ]]], "BCI"]
Out[7]=

Show the abstract proof network:

In[8]:=
proof["ProofGraph"]
Out[8]=

Scope (7) 

Show that a combinator equivalence proposition cannot be derived from a given combinatory calculus:

In[9]:=
ResourceFunction["FindCombinatorProof"][
 s[s][s][k] == s[s][k][s], <|"Combinators" -> {s, k}, "Rules" -> {s[x][y][z] == x[z][y[z]], k[x][y] == x}|>]
Out[9]=

Named Combinatory Calculi (6) 

FindCombinatorProof supports a variety of named combinatory calculi, including the single-variable fixed-point (y) combinator:

In[10]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalY][\[FormalF]] == \[FormalF][\[FormalF][\[FormalF][\[FormalY][\[FormalF]]]]], "Y"]
Out[10]=

The two-variable fixed-point (y) combinator:

In[11]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalY][\[FormalF]][\[FormalY][\[FormalX]]] == \[FormalY][\[FormalF]][\[FormalX][\[FormalX][\[FormalX][\[FormalY][\[FormalX]]]]]], "Y2"]
Out[11]=

The S-K calculus:

In[12]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalS][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalS]][\[FormalS]][\[FormalK]] == \[FormalS][\[FormalS][\[FormalS]]][\[FormalK]][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]], "SK"]
Out[12]=

The S-K-I calculus:

In[13]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalS][\[FormalK][\[FormalS]][\[FormalI]]][\[FormalS][\[FormalK]][\[FormalK]][\[FormalI]]][\[FormalX]][\[FormalY]] == \[FormalX][\[FormalY]][\[FormalX][\[FormalY]]], "SKI"]
Out[13]=

Schönfinkel's B and C combinators:

In[14]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalC][\[FormalK]][\[FormalB][\[FormalX]][\[FormalK]][\[FormalZ]]][\[FormalY]] == \[FormalK][\[FormalY]][\[FormalX][\[FormalK][\[FormalZ]]]], "BC"]
Out[14]=

The B-C-I calculus:

In[15]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalC][\[FormalI]][\[FormalB][\[FormalX]][\[FormalI]][\[FormalZ]]][\[FormalY]] == \[FormalY][\[FormalX][\[FormalZ]]], "BCI"]
Out[15]=

Initial Conditions (1) 

FindCombinatorProof accepts both individual theorems and lists of theorems:

In[16]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalS][\[FormalK][\[FormalS]][\[FormalI]]][\[FormalS][\[FormalK]][\[FormalK]][\[FormalI]]][\[FormalX]][\[FormalY]] == \[FormalX][\[FormalY]][\[FormalX][\[FormalY]]], "SKI"]
Out[16]=
In[17]:=
ResourceFunction[
 "FindCombinatorProof"][{\[FormalS][\[FormalK][\[FormalS]][\[FormalI]]][\[FormalS][\[FormalK]][\[FormalK]][\[FormalI]]][\[FormalX]][\[FormalY]] == \[FormalX][\[FormalY]][\[FormalX][\[FormalY]]], \[FormalS][\[FormalK][\[FormalS]][\[FormalI]]][\[FormalS][\[FormalK]][\[FormalK]][\[FormalI]]][\[FormalY]][\[FormalX]] == \[FormalY][\[FormalX]][\[FormalY][\[FormalX]]]}, "SKI"]
Out[17]=

Options (1) 

TimeConstraint (1) 

Use TimeConstraintt to limit the computation time to t seconds:

In[18]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalS][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalS]][\[FormalS]][\[FormalK]] == \[FormalS][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalS][\[FormalS]][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]]]]], "SK", TimeConstraint -> 0.001]
Out[18]=
In[19]:=
ResourceFunction[
  "FindCombinatorProof"][\[FormalS][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalS]][\[FormalS]][\[FormalK]] == \[FormalS][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalS][\[FormalS]][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]]]]], "SK"] // AbsoluteTiming
Out[19]=

Properties and Relations (1) 

FindCombinatorProof will return a proof object for a particular theorem if and only if the associated path exists in the corresponding multiway system:

In[20]:=
ResourceFunction[
 "FindCombinatorProof"][\[FormalS][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalS]][\[FormalS]][\[FormalK]] == \[FormalS][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalS]][\[FormalS][\[FormalS][\[FormalS]]]][\[FormalK]]]][\[FormalS][\[FormalS]][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]][\[FormalK][\[FormalK][\[FormalS][\[FormalK]][\[FormalS][\[FormalS][\[FormalS]]][\[FormalK]]]]]]]], "SK"]
Out[20]=
In[21]:=
mwGraph = ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_] :> x[z][y[z]], k[x_][y_] :> x}, s[s[s[s]]][s][s][k], 10, "StatesGraphStructure"]
Out[21]=
In[22]:=
path = FindShortestPath[mwGraph, ToString[s[s[s[s]]][s][s][k]], ToString[s[k[s[s][s[s[s]]][k]]][
    k[k[s[s][s[s[s]]][k]]][
     s[s][k[s[k][s[s[s]][k]]]][k[k[s[k][s[s[s]][k]]]]]]]]]
Out[22]=
In[23]:=
HighlightGraph[mwGraph, Subgraph[mwGraph, path]]
Out[23]=

Resource History

Source Metadata

Related Resources

License Information