WOLFRAM NOTEBOOK

Combinators in FindEquationalProof

WRI, December 2019
• Following Roman temporary proposal, we use LeftTee as application operator, to have the proper left-associative typesetting. The S expression in the third axiom looks great. We use Id instead of the more standard I for obvious reasons.
In[]:=
CombinatorAxioms={​​ForAll[{x},LeftTee[Id,x]x],​​ForAll[{x,y},LeftTee[LeftTee[K,x],y]x],​​ForAll[{x,y,z},LeftTee[LeftTee[LeftTee[S,x],y],z]LeftTee[LeftTee[x,z],LeftTee[y,z]]]​​}
Out[]=
∀
{x}
(Id⊣x)x,
∀
{x,y}
(K⊣x⊣y)x,
∀
{x,y,z}
(S⊣x⊣y⊣z)(x⊣z⊣(y⊣z))
• I have the impression that LeftTee has too low precedence, so an outermost parenthesis is always needed. Compare to something like Apply:
Precedence/@{LeftTee,Equal,Apply}
{190.,290.,620.}
• Two results given in the [wikipedia] page on Combinatory Logic:
In[]:=
thm1=ForAll[{x},LeftTee[LeftTee[LeftTee[S,K],K],x]x]
Out[]=
∀
{x}
(S⊣K⊣K⊣x)x
proof1=FindEquationalProof[thm1,CombinatorAxioms]
ProofObject
Logic: EquationalLogic
Steps: 5
Theorem:
∀
{x}
(S⊣K⊣K⊣x)x
thm2=LeftTee[LeftTee[LeftTee[LeftTee[S,LeftTee[K,LeftTee[S,Id]]],LeftTee[LeftTee[S,LeftTee[K,K]],Id]],x],y]LeftTee[y,x]
(S⊣(K⊣(S⊣Id))⊣(S⊣(K⊣K)⊣Id)⊣x⊣y)(y⊣x)
proof2=FindEquationalProof[thm2,CombinatorAxioms]
ProofObject
Logic: EquationalLogic
Steps: 12
Theorem: (S⊣(K⊣(S⊣Id))⊣(S⊣(K⊣K)⊣Id)⊣x⊣y)(y⊣x)
Hover over the nodes to follow the evolution of the expressions:
proof["ProofGraph"]
Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.