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

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

In[]:=

(Id⊣x)x,(K⊣x⊣y)x,(S⊣x⊣y⊣z)(x⊣z⊣(y⊣z))

∀

{x}

∀

{x,y}

∀

{x,y,z}

Out[]=

• 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.}

thm1=ForAll[{x},LeftTee[LeftTee[LeftTee[S,K],K],x]x]

In[]:=

∀

{x}

Out[]=

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