Searching for Non-Trivial Combinator Equivalences

In[]:=
s7={s[s[s]][s][s][s][s],s[s][s][s[s]][s][s]};
In[]:=
s8={s[s[s[s][s]]][s][s][s],s[s[s[s[s][s]]]][s][s],s[s[s]][s][s][s][s][s],s[s[s[s]][s][s][s][s]],s[s[s[s]][s][s]][s][s],s[s[s[s]][s]][s][s][s],s[s[s[s[s]][s]]][s][s],s[s[s[s]]][s][s][s][s],s[s[s[s[s]]][s]][s][s],s[s[s[s[s]]]][s][s][s],s[s][s][s[s]][s][s][s],s[s[s][s][s[s]][s][s]],s[s[s][s][s[s]]][s][s],s[s[s]][s[s]][s][s][s],s[s[s[s]][s[s]]][s][s],s[s[s]][s][s[s]][s][s],s[s[s[s]]][s[s]][s][s],s[s][s][s[s][s]][s][s],s[s][s][s[s[s]]][s][s],s[s[s]][s[s[s]]][s][s],s[s[s][s]][s][s[s]][s],s[s[s[s][s]]][s[s]][s],s[s[s]][s][s][s[s]][s],s[s[s[s]]][s][s[s]][s],s[s][s][s[s]][s[s]][s],s[s][s][s[s[s][s]]][s],s[s[s]][s][s[s][s]][s],s[s][s][s[s[s]][s]][s],s[s[s]][s][s[s[s]]][s],s[s][s][s[s[s[s]]]][s],s[s[s[s][s]]][s][s[s]],s[s[s]][s][s][s][s[s]],s[s[s[s]][s]][s][s[s]],s[s[s[s]]][s][s][s[s]],s[s][s][s[s]][s][s[s]],s[s[s]][s[s]][s][s[s]],s[s[s]][s][s[s]][s[s]],s[s][s][s[s][s]][s[s]],s[s][s][s[s[s]]][s[s]],s[s[s][s]][s][s[s][s]],s[s[s][s]][s][s[s[s]]]};
In[]:=
In[]:=
ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},s[s[s]][s][s][s][s],12]
Out[]=
{{s[s[s]][s][s][s][s]},{s[s][s][s[s]][s][s]},{s[s[s]][s[s[s]]][s][s]},{s[s][s][s[s[s]][s]][s]},{s[s[s[s]][s]][s[s[s[s]][s]]][s]},{s[s[s]][s][s][s[s[s[s]][s]][s]]},{s[s][s][s[s]][s[s[s[s]][s]][s]]},{s[s[s]][s[s[s]]][s[s[s[s]][s]][s]]},{s[s][s[s[s[s]][s]][s]][s[s[s]][s[s[s[s]][s]][s]]]},{s[s[s[s]][s[s[s[s]][s]][s]]][s[s[s[s]][s]][s][s[s[s]][s[s[s[s]][s]][s]]]]},{s[s[s[s]][s[s[s[s]][s]][s]]][s[s[s]][s][s[s[s]][s[s[s[s]][s]][s]]][s[s[s[s]][s[s[s[s]][s]][s]]]]]},{s[s[s[s]][s[s[s[s]][s]][s]]][s[s][s[s[s]][s[s[s[s]][s]][s]]][s[s[s[s]][s[s[s[s]][s]][s]]]][s[s[s[s]][s[s[s[s]][s]][s]]]]]},{s[s[s[s]][s[s[s[s]][s]][s]]][s[s[s[s[s]][s[s[s[s]][s]][s]]]][s[s[s]][s[s[s[s]][s]][s]][s[s[s[s]][s[s[s[s]][s]][s]]]]][s[s[s[s]][s[s[s[s]][s]][s]]]]]}}
In[]:=
checkIntersect[{e1_,e2_},t_]:=With[{mw=Flatten[ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},#,t]]&/@{e1,e2}},If[MemberQ[e1,mw[[2]]]||MemberQ[e2,mw[[1]]],-1,If[IntersectingQ[mw[[1]],mw[[2]]],1,0]]]
In[]:=
findIntersection[{e1_,e2_},t_]:=Module[{mw=ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},#,t]&/@{e1,e2},fmw},fmw=Flatten/@mw;If[MemberQ[e1,fmw[[2]]]||MemberQ[e2,fmw[[1]]],None,If[IntersectingQ[fmw[[1]],fmw[[2]]],With[{i=Intersection[fmw[[1]],fmw[[2]]]},Flatten[{First/@Position[mw[[1]],#],First/@Position[mw[[1]],#]}]&/@i],None]]]
In[]:=
findIntersection[{s[s[s]][s][s][s][s],s[s][s][s[s]][s][s]},10]
Out[]=
{{2,2},{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11}}
In[]:=
Table[#TimeConstrained[findIntersection[#,12],10]&[RandomSample[sk8,2]],20]
Out[]=
{{s[s[s][k]][s][s[s][s]],s[s][k][s[s[s][k]]][s]}None,{s[s[s]][s][s][s][k[s]],s[s[s]][s[s[s]]][s][s]}None,{s[s[s][s][s[s]]][k][s],s[s[s[s]][s][s]][s][s]}None,{s[s[s[s[s]]][s]][s][s],k[s[s][s][s[s]][s][s]]}None,{s[s[s][k]][s][s[s][k]],s[s[s[s]][s]][s][s][s]}None,{s[s][s][s[s[s][s]]][s],s[s][s][s[s]][s][k[s]]}None,{s[s[s]][s[s[s]]][s][s],k[s[s][s][s[s]][s][s]]}None,{s[s][s][s[s][s]][s][s],s[s[s[s[s]][s]]][s][s]}None,{s[s[s]][s][s[s][s]][s],s[s][s][s[s[s][s]]][s]}None,{s[s[s[s]][s][s][s][s]],s[s][s][s[s[s]]][s[s]]}None,{s[s[s]][s][s][s][k[s]],s[s[s[s]]][s[s]][s][k]}None,{s[s[s][s][s[s]][s][s]],s[s[s]][s][s[s[s]]][k]}None,{s[s[s[s][s]]][s][s][s],s[s][s][s[s][s]][s][s]}None,{s[s][s][s[s[s[s]]]][k],s[s[s][k]][s][s[s][k]]}None,{s[s[s[s][s]]][s][s][k],s[s][k][s[s]][s][s][s]}None,{s[s[s[s]][s][s]][s][s],s[s[s[s[s][s]]]][s][s]}None,{s[s][s][s[s]][s][s[k]],s[s][s][s[s[s[s]]]][k]}None,{s[s][k][s[s[s][s]]][s],s[s[s]][s][s[s][s]][s]}None,{s[s[s[s][k]]][s[s]][s],s[s][s][s[s[s][s]]][k]}None,{s[s[s][s]][s][s[s][s]],s[s][s][s[s[s][k]]][s]}None}
In[]:=
Join[s7,sk8]//Length
Out[]=
75
In[]:=
75^2
Out[]=
5625
In[]:=
ResourceFunction["ParallelMapMonitored"][#TimeConstrained[findIntersection[#,12],10]&,Tuples[Join[s7,sk8],2]]
(kernel 69)
Syntax::com:Warning: comma encountered with no adjacent expression. The expression will be treated as Null. (line 2 of "/tmp/Wolfram/ResourceSystemClient/LockFiles/.25e14716-95a2-4392-85ce-33c6b4d65c84339e580ce5322a43").
Parallel`Protected`PacketHandler
::default
:Unhandled packet SyntaxPacket[3425] received and discarded from KernelObject
Name: threadripper
KernelID: 79
.
​
Parallel`Protected`PacketHandler
::default
:Unhandled packet SyntaxPacket[53207] received and discarded from KernelObject
Name: threadripper
KernelID: 73
.
​
(kernel 69)
IntersectingQ::heads:Heads $Failed and List at positions 1 and 2 are expected to be the same.
Parallel`Protected`PacketHandler
::default
:Unhandled packet SyntaxPacket[211677] received and discarded from KernelObject
Name: threadripper
KernelID: 91
.
​
General
:Further output of Parallel`Protected`PacketHandler::default will be suppressed during this calculation.
LinkObject
:Unable to communicate with closed link LinkObject[56289@10.20.50.7,56290@10.20.50.7,7087,82].
KernelObject
:Subkernel connected through KernelObject
Name: threadripper
KernelID: 72
 appears dead.
Parallel`Developer`QueueRun
::req
:Requeueing evaluations {12393} assigned to KernelObject
Name: threadripper
State: defunct
.
​
LaunchKernels
:Kernel KernelObject
Name: threadripper
State: defunct
 resurrected as KernelObject
Name: threadripper
KernelID: 94
.
LinkObject
:Unable to communicate with closed link LinkObject[56293@10.20.50.7,56294@10.20.50.7,7089,84].
KernelObject
:Subkernel connected through KernelObject
Name: threadripper
KernelID: 74
 appears dead.
Parallel`Developer`QueueRun
::req
:Requeueing evaluations {12586} assigned to KernelObject
Name: threadripper
State: defunct
.
​
LaunchKernels
:Kernel KernelObject
Name: threadripper
State: defunct
 resurrected as KernelObject
Name: threadripper
KernelID: 95
.
IntersectingQ
:Heads $Failed and List at positions 1 and 2 are expected to be the same.
Out[]=
{{s[s[s]][s][s][s][s],s[s[s]][s][s][s][s]}{{2,2},{1,1},{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13}},{s[s[s]][s][s][s][s],s[s][s][s[s]][s][s]}{{2,2},{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13}},
⋯5622⋯
,{k[s[s][s][s[s]][s][s]],k[s[s][s][s[s]][s][s]]}{{1,1},{3,3},{2,2},{6,6},{5,5},{4,4},{7,7},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13},{13,13}}}
large output
show less
show more
show all
set size limit...
In[]:=
inters=DeleteCases[%,_None];
In[]:=
Length[inters]
Out[]=
470
In[]:=
inters
Out[]=
{{s[s[s]][s][s][s][s],s[s[s]][s][s][s][s]}{{2,2},{1,1},{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13}},{s[s[s]][s][s][s][s],s[s][s][s[s]][s][s]}{{2,2},{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13}},{s[s[s]][s][s][s][s],s[s[s]][s[s[s]]][s][s]}{{4,4},{3,3},{7,7},{6,6},{5,5},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13}},
⋯464⋯
,{k[s[s][s][s[s]][s][s]],s[s[s]][s][s[s][k]][k]}$Aborted,{k[s[s][s][s[s]][s][s]],k[s[s[s]][s][s][s][s]]}{{1,1},{3,3},{2,2},{6,6},{5,5},{4,4},{7,7},{8,8},{9,9},{10,10},{11,11},{12,12}},{k[s[s][s][s[s]][s][s]],k[s[s][s][s[s]][s][s]]}{{1,1},{3,3},{2,2},{6,6},{5,5},{4,4},{7,7},{8,8},{9,9},{10,10},{11,11},{12,12},{13,13},{13,13}}}
large output
show less
show more
show all
set size limit...
In[]:=
Length[Last[#]]&/@%
Out[]=
{13,12,11,10,0,0,10,12,14,13,12,0,0,10,128,127,0,0,286,285,0,0,20,19,0,0,13,3,12,0,0,33,31,30,29,0,0,61,60,59,0,0,160,159,0,0,597,596,0,0,130,129,128,0,0,538,537,0,0,19,30,0,0,12,14,0,0,31,73,71,71,0,0,49,48,0,0,14,13,12,0,0,596,1928,0,0,765,764,0,0,48,107,0,0,962,0,0,11,13,17,16,0,0,9,127,340,0,0,75,74,0,0,60,113,112,0,0,537,1145,0,0,59,112,212,0,0,19,0,0,764,1272,0,0,10,12,16,26,0,0,8,1930,0,0,200,78,0,0,285,937,0,0,30,71,72,71,0,0,159,655,0,0,129,379,378,0,0,29,71,71,191,0,0,13,19,18,0,0,128,378,1182,0,0,12,18,34,0,0,394,0,0,74,225,0,0,782,0,0,137,136,0,0,597,596,0,0,596,1928,0,0,766,765,0,0,962,0,0,136,371,0,0,19,0,0,765,1291,0,0,2642,0,0,222,1157,0,0,101,100,0,0,100,306,0,0,1060,0,0,1,29,27,0,26,25,0,27,46,0,44,44,0,44,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,26,44,0,45,44,0,25,44,0,44,74,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,297,296,0,0,296,870,0,0,1678,10,10,9,8,0,0,33,200,0,0,1658,0,0,980,222,0,0,1738,0,0,1471,0,0,2064,1,0,0,2655,0,0,13,12,0,0,12,14}
In[]:=
Position[%,1]
Out[]=
{{246},{459}}
In[]:=
inters[[246]]
Out[]=
{s[s[s][s]][s][s[s][k]],s[s][k][s[s[s][k]]][k]}{{3,3}}
In[]:=
inters[[459]]
Out[]=
{s[s][k][s[s[s][k]]][k],s[s[s][s]][s][s[s][k]]}{{13,13}}
In[]:=
ResourceFunction["MultiwayCombinator"][{s[x_][y_][z_]x[z][y[z]],k[x_][y_]x},#,12,"StatesGraphStructure"]&/@{s[s][k][s[s[s][k]]][k],s[s[s][s]][s][s[s][k]]}
Out[]=

,


Proof

[ Result took 6 hrs ]