Combinators in FindEquationalProof
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[]=
(Id⊣x)x,(K⊣x⊣y)x,(S⊣x⊣y⊣z)(x⊣z⊣(y⊣z))
∀
{x}
∀
{x,y}
∀
{x,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.}
In[]:=
thm1=ForAll[{x},LeftTee[LeftTee[LeftTee[S,K],K],x]x]
Out[]=
∀
{x}
proof1=FindEquationalProof[thm1,CombinatorAxioms]
ProofObject
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
Hover over the nodes to follow the evolution of the expressions:
proof["ProofGraph"]