λ calculus by Mathematica (program編)

ClearAll["Global`*"]

初めに

[1] Mathematica(v11.1) によるλ計算の簡約器です．実行プログラムは reduce[string]　の一個です．このnotebookの一番最後のコマンドです．λ計算ではやはり自分でテキストを入力したいので　Manipulate　は使えませんでした．reduce["(λx.(xy))a"]　の様に使用します．本当は "λ" の代わりに "\" を使いたかったのですが, Mathematica では，"\" はエスケープ文字なので使えませんでした．なおλ の入力は Esc+lambda+Esc で簡単に入力できます(windows の場合)．最左簡約(normal order)で，簡約のリスト＆結果を出力します．また通常の簡約の他にマクロも使えて追加もできます．マクロについては「マクロ編」に詳しく書きました．（このnotebookのダウンロード元と同じページに置いて有ります．)
[2]「C言語による計算の理論」（鹿島亮著） を読んでλ計算に興味を持ち，その勉強のために作りました．λ計算の書式はこの本に依っています．この本でのルールは
    （１）変数はラムダ項である.  （２）M と N がラムダ項なら (MN) もラムダ項である. （３）Mがラムダ項でxが変数なら (λx.M) もラムダ項である.  (４)以上の(1)~(3) で得られるものだけがラムダ項である.
    です，（このプログラムでは変数は一文字のアルファベットのみです．） さらに次の省略が可能としてます．
    ●一番外側の括弧を省略する  ● (((((Subscript[M, 1]))(Subscript[M, 2]))(Subscript[M, 3])...)(Subscript[M, n])) という形の連続した関数適用を (Subscript[M, 1])(Subscript[M, 2])(Subscript[M, 3])...(Subscript[M, n]) と書く  ● ((Subscript[λx, 1.])((Subscript[λx, 2.])(...(Subscript[λx, n.])M))) という形の連続した関数抽象を (Subscript[λx, 1])(Subscript[x, 2...])(Subscript[x, n.])M と書く
 以上が本に述べられた規則の全てです．が，ここでは (Subscript[λx, .])(MN) の括弧を省略した (Subscript[λx, .])MN や λx.p(λy.xy) の代わりに λx.pλy.xy　と書くこともOK としました．最後の例をご覧になればすぐお分かりになると思います．
[3]驚いたのは Mathematica の通常のプログラミング言語としての機能の凄さです．おかげさまでかなり短く仕上げることができました．今回はじめてMathematicaで文字列処理を本格的にしましたが，その「文字列パターン」は非常にパワフルでした．(Wolframによると)正規表現とおなじ事ができてかつ分かりやすいそうです．しかし余りにも「文字列パターン」が凄すぎ，対応する括弧を見つけるにも使ってやろうとして，時間をかなり無駄にしました．
[4]作った動機は, 1つ目はλ計算の勉強のため(やはり自分で作るとよく分かる)． 2つ目は「やはりMathematica でλしたい」というMathematica愛です．正直言ってブラウザ上で動くよく出来たプログラムに比べると使い勝手においても機能においても勝負になりません．（そもそもMathematicaを持っていないと使えないし，後述するラムダフレンズの様にマウスで簡約基を選んだりもできない)．メリットは「Mathematica programである」という一点だけです．これを見てらっしゃる方もやはりMathematica fan だと思います．もし 単純に良い簡約器を探しておられるなら，私は日本の「ラムダフレンズ」が一番良いと思います．特にβ基をワンクリックで選べるのがすごいです．これをMathematica で実現しようとすると，非常に大変でしょう．作者のλ愛が感じられるプログラムで4000行?もコードを書いているそうです．私はいくらなんでもそこまでのめり込めないので，ひと月弱で取り敢えず仕上げました．あまりバグ取りもしていないので沢山虫がいると思います．^_^;  もし遭遇しましたらできればこちらまでお知らせ下さい．あるいはご自分で修正してください．その場合はご一報いただけると幸いです．
なお作成には　ラムダフレンズと wikipedia(英語版) には特にお世話になりました．ラムダフレンズさんには動作の検証で，マクロの説明はWikiさんに．下に両方のリンクを張っておきます．有難うございました． (2022年6月20日　生越　茂樹)

Program

主プログラムの依存関係は 　alphafor1 < unitAlpha < unitBeta < stringBeta <  reduce　となっています． この間に補助プログラムとマクロのプログラムが入っています．

[1]. 補助プログラム

range

range[x_]:=Range@@x;
range[x_/;x=={}]:={};
range[listoflist_?MatrixQ]:=Union[Flatten[range/@listoflist]];
eitherInrangeQ[pos_List,bracket_List]:=AnyTrue[pos,MemberQ[range[bracket],#]&](*posの要素のいずれかが bracket の中に入っているか否か？*)

例

range[{{2,5},{10,12}}]
{1,3,5}~eitherInrangeQ~{2,5}

ちょっとだけ構文解析１(括弧，関数のリスト作成)

(*cket は 文sのn番目のpositionにある左括弧(bra)に対応する右括弧(cket)のsに於けるpositionを求める.
cketはmakeBra2cketの中とmakeBra2cketを使用している多くのコマンド中でのみ用いる*)

cket[n_]:=Block[{m,k,index},
m=FirstPosition[kakko,n][[1]];(*kakko,suretsu は makeBra2cket の中で定義されている*)
index=Range[m+1,Length[kakko]];
k=SelectFirst[index,Plus@@Take[suretsu,{m,#}]==0&];(*while文でも書ける*)
Return[kakko[[k]]]
]
(*makeBra2cketは左括弧と右括弧のAssociationを与える*)
makeBra2cket[s_String]:=Block[{left,right,kakko,suretsu,bra2cket},
left=StringPosition[s,"("][[All,1]];
right=StringPosition[s,")"][[All,1]];
kakko=Union[left,right];
suretsu=kakko/.{x_/;MemberQ[left,x]->1,x_/;MemberQ[right,x]->-1};
Return[Association[#->cket[#]&/@left]]
]
(*makeFunctionListは関数の左括弧,右括弧,変数,変数の入っている場所,本体の入っている場所を与える.ただし，全体が一つの関数でかつ両端に括弧のないときはカウントされない．しかし，redexに全体関数が入ることはないので redex には関係ない．*)
makeFunctionList[s_String]:=Block[{bra2cket,yen,vars,functions,bodys},
bra2cket=makeBra2cket[s];
yen=StringPosition[s,Shortest["(λ"~~LetterCharacter ..~~"."]];(*(λ..(Subscript[v, 1]).. . の左括弧の位置．例えば{{1,3},{5,7},{11,13}}*)
vars=StringCases[s,Shortest["(λ"~~x__~~"."]->Characters[x]];
functions={#1,bra2cket[#1]}&/@yen[[All,1]];
bodys=MapThread[{#1[[2]]+1,#2[[2]]}&,{yen,functions}];
Return[MapThread[{#1,#2,#3,#4}&,{functions,vars,yen,bodys}]]
]

例

s="(λx.((λy.(xy))y))";
makeBra2cket[s]
makeFunctionList[s]

ちょっとだけ構文解析2 (β基(βredex)のリスト作成)

makeRedexListはredexの「関数」と「代入される式」の場所を与える

抽出は (λx.M)の右側に “)” が無い事で判定．従って最初に余分な括弧を取ることが必須．しかしこれはreduceで最初の最初にやっているのでここでは不要

getMigidonariOfCket は makeRedexList の中でのみ使う． left, bra2cket は makeRedxListの中で与えられる

redexは関数と違い (λ x..M)N の様に必ずλの左に括弧がついているので，数え漏らしがない．

getMigidonariOfCket[pos_Integer]:=If[MemberQ[left,pos],{pos,bra2cket[pos]},{pos,pos}]

makeRedexList[s_String]:=Block[{bra2cket,left,right,funcranges,oks,okfuncs,βredex,migidonari},
(*s=deleteDuplicates[str];*)(*余分のかっこを除く*)
bra2cket=makeBra2cket[s];
left=Keys[bra2cket];
right=Values[bra2cket];
funcranges=makeFunctionList[s][[All,1]];
oks=Complement[Range[StringLength[s]],right];(*右括弧と文末を除いたpositionの集合*)
okfuncs=Select[funcranges,MemberQ[oks,#[[2]]+1]&];(*右括弧の隣がokに入っている⇔β簡約可能functionの集合*)
βredex=If[okfuncs=={},{{}},(*StringBeta中でβredexはMatrix*)
migidonari=getMigidonariOfCket[#[[2]]+1]&/@okfuncs;
βredex=MapThread[{#1,#2}&,{okfuncs,migidonari}]];
Return[βredex]
];

findLeftMostRedex[s_String]:=Block[{bra2cket,left,right,funcranges,oks,βredex,migidonari},
(*s=deleteDuplicates[str];*)(*余分のかっこを除く*)
bra2cket=makeBra2cket[s];
left=Keys[bra2cket];
right=Values[bra2cket];
funcranges=makeFunctionList[s][[All,1]];
oks=Complement[Range[StringLength[s]],right];(*右括弧と文末を除いたpositionの集合*)
okfunc=SelectFirst[funcranges,MemberQ[oks,#[[2]]+1]&];(*右括弧の隣がokに入っている⇔β簡約可能functionのうち一番左*)
βredex=If[!ListQ[okfunc],{},(*StringBeta中でβredexはMatrixでない{{}}*)
migidonari=getMigidonariOfCket[okfunc[[2]]+1];
βredex={okfunc,migidonari}];
Return[βredex]
];

例

s="(λx.((λy.(xy))))(ay)";
makeRedexList[s][[1]]
StringTake[s,#]&/@%
findLeftMostRedex[s]

不要な括弧を取り除く

「deleteDeplicates」は (((A)))→(A) の様に 2重以上の括弧を消す
「deleteBothEnds」は 両端の括弧を消す
「deleteKakko」は両方の括弧を消す

deleteDuplicates[s_?(StringFreeQ[#,"("~~___~~")"]&)]:=s;
deleteBothEnds[s_?(StringFreeQ[#,"("~~___~~")"]&)]:=s

deleteDuplicates[s_String]:=Block[{bra2cket,brackets,delIndex,delPos},
bra2cket=makeBra2cket[s];
brackets=MapThread[{#1,#2}&,{Keys[bra2cket],Values[bra2cket]}];
(*対応している左右括弧のpositionのセット. s="a(b((((c)(de)))))"の時，{{2,17},{4,16},{5,15},{6,14},{7,9},{10,13}}*)
delIndex=Select[Range[Length[brackets]-1],brackets[[#+1]]-brackets[[#]]=={1,-1}&];
(*delete index. 消去スべき左右括弧のbracketsに於けるindex. 上の例では{2,3,4}*)
delPos=brackets[[delIndex]];
(*delete position. 消去スべき左右括弧のsに於けるposition. 上の例では{4,5,6,16,15,14}*)
StringReplacePart[s,"",{#,#}&/@Flatten[delPos]]
]
deleteBothEnds[s_String]:=Block[{bra2cket,firstkey,bookends},
bra2cket=makeBra2cket[s];
firstkey=Keys[bra2cket][[1]];
bookends={1,StringLength[s]};
If[{firstkey,bra2cket[firstkey]}==bookends,StringReplacePart[s,"",{#,#}&/@bookends],s]
]
deleteKakko[s_String]:=deleteBothEnds[deleteDuplicates[s]];

例

deleteDuplicates["((((ay)((λx.y)))((ay))))"]
deleteBothEnds[%]

省略された入力に対して 括弧を補う

関数の右端はλの入っているもっとも内側のかっこ（右括弧）まで

関数のBodyの始まりは”λ”~~LetterWords..~~”.” のドットから

関数全体の始まりはλの左から

inRangeQ[x_Integer]:=Select[brackets,MemberQ[range[#],x]&];(*xを含んでいるbracketをbracketsから選ぶ．bracketsFormattingの中で使う*)
bracketsFormatting[str_String]:=Block[{s,bra2cket,brackets,yens,coveringBrackets,mKakko,bodyhKakko,funchKakko,hKakko},
s=StringReplace[str,Whitespace->""];
s="("<>s<>")";
bra2cket=makeBra2cket[s];
brackets=MapThread[{#1,#2}&,{Keys[bra2cket],Values[bra2cket]}];
yens=StringPosition[s,"λ"][[All,1]];
coveringBrackets=inRangeQ/@yens;
mKakko=Min/@(#[[All,2]]&/@coveringBrackets);
s=StringInsert[s,")",mKakko];
hKakko=StringPosition[s,"λ"][[All,1]];
s=StringInsert[s,"(",hKakko];
Return[deleteKakko[s]]
]

(*bracketsFormatting2[str_String]:=Block[{s,bra2cket,brackets,yens,coveringBrackets,mKakko,bodyhKakko,funchKakko,hKakko},
s=StringReplace[str,Whitespace->""];
s="("<>s<>")";
bra2cket=makeBra2cket[s];
brackets=MapThread[{#1,#2}&,{Keys[bra2cket],Values[bra2cket]}];
yens=StringPosition[s,"λ"][[All,1]];
coveringBrackets=inRangeQ/@yens;
mKakko=Min/@(#[[All,2]]&/@coveringBrackets);
s=StringInsert[s,"))",mKakko];
bodyhKakko=StringPosition[s,"."][[All,1]]+1;
funchKakko=StringPosition[s,"λ"][[All,1]];
hKakko=bodyhKakko~Join~funchKakko;
s=StringInsert[s,"(",hKakko];
Return[deleteKakko[s]]
]*)

MapThread[(#1^2+(#2)^3)&,{{1,3},{2,4}}]

bracketsFormatting["λx.xλx.xxλx.x"]

bracketsFormatting["λx.pλy.xy"]

s内の自由変数の位置を見つける.(右括弧の方が多くてもOK)

freePosは，sの中の自由変数varのpositionを見つける.

freeQは,sの中に自由変数 var があるか？

freePos[s_String,var_String]:=Block[{bra2cket,functions,bindedIfinside,allpositions},
functions=makeFunctionList[s];
bindedIfinside=Select[functions,MemberQ[#[[2]],var]&][[All,1]];
allpositions=StringPosition[s,var][[All,1]];
Select[allpositions,!MemberQ[range[bindedIfinside],#]&]
]
freeQ[s_String,var_String]:=freePos[s,var]!={};

例

freePos["λx.((λyz.(xy))(λy.y)y)(ay)","y"]

[2]. unitAlpha は redex ((Subscript[λx, 1])...(Subscript[x, m]).M)Lの α変換. 
-入力は((Subscript[λx, 1])...(Subscript[x, m]).M)と「Lの自由変数」．出力は ((Subscript[λx, 1])...(Subscript[x, m]).M)をα変換したもの.unitBeta中で使うので変数freeX1，alphabetsはunitBetaから貰う-

(*ClearAll["Global`*"]*)

1. リストfreeX1は，(Subscript[Mの中の自由変数x, 1])のposition の集まり．β変換で LはfreeX1に入る.

2.(Subscript[変数x, i])はLの自由変数とする．このとき freex1が入る場所posを囲んでいる関数 (λ..(Subscript[x, i])..。..(pos).. (Subscript[x, i])..) に入っている束縛(Subscript[変数x, i])の場所を求めてα変換する．

3.新しい変数はredexの全変数と一致しない様にしている．通常はalphabetは不足しないはず．

4. R= ((Subscript[λx, 1])...(Subscript[x, m]).M)L 全体がある関数の中に入っている場合でも，Rのα変換は Rについてのみ考えれば良い.これはうれしい(^_^)

(*unitalpha[F,Lの自由変数全てのリスト],alphafor1[F,Lの自由変数の内1つ]*)
alphafor1[s_String,v_String]:=Block[{functions,rangeMaybeIncluded,rangeExcluded,rangeIncluded,alphaVariables,u,t,end},
functions=makeFunctionList[s];
rangeIncluded=Select[functions,(MemberQ[#[[2]],v])&&(freeX1~eitherInrangeQ~#[[1]])&&(freeQ[StringTake[s,#[[4]]],v])&][[All,1]]//range;
alphaVariables=Select[StringPosition[s,v][[All,1]],MemberQ[rangeIncluded,#]&];
If[alphaVariables!={},
    u=SelectFirst[alphabets,StringFreeQ[s,#]&];
    t=Return[StringReplacePart[s,u,{#,#}&/@alphaVariables]];
,t=s];
Return[t]
]
unitAlpha[s_String,vars_List]:=Fold[alphafor1,s,vars]

例

alphabets = Select[Alphabet[], StringFreeQ["xyz", #] &];
s1 = "(λxzy.xyz(λy.xz)y)"
freeX1 = freePos[StringDrop[s1, 6], "x"] + 6;
alphafor1[s1, "y"]
unitAlpha[s1, {"y","z"}]

s2="(λx.(λzy.(xy)(λy.x)y(λy.x)(λy.y)))";
freeX1=freePos[StringDrop[s2,4],"x"]+4;
unitAlpha[s2,{"y","z"}]

[3].unitBetaは redex=(λx.. .M)L に関する β 変換

1. (λx.(λy.M(y)))(yz)などをα変換して (λx.(λa.M(a)))(yz)に直す

2.　redex: FL= (λx.. .M)L={λx...M,L}に対し，Fのxの「束縛」変数=Mの中にある「自由」変数xをLに置き換える

3. 入力されるのは {(λx...M),L} の形のみ

unitBeta[set_List]:=Block[{f,f1,f2,x1,vars,dot,freeX1,alphabets,freeVarL,beta},
f=set[[1]];L=set[[2]]; (*例s="(λx.(λx.x)(λx.x)x)",L="z"のとき，s1=(λx.,s2=(λx.x)(λx.x)x)*)
dot=StringPosition[f,"."][[1,1]];(*最初のdotの場所*)
f1=StringTake[f,dot];(*最初のdotまでの文*)
f2=StringDrop[f,dot];(*最初のdot以降の文*)
x1=StringCases[f1,"(λ"~~x_->x][[1]];(*fの最初の変数がx1*)
freeX1=freePos[f2,x1];(*s2の中の「自由」変数x1の位置のリスト*)
alphabets=Select[Alphabet[]~Join~ToUpperCase[Alphabet[]],StringFreeQ[L,#]&];
freeVarL=Select[StringCases[L,LetterCharacter?(UnsameQ[#,"λ"]&)],freeQ[L,#]&]//Union;(*Lの自由変数のリスト*)
f=unitAlpha[f,freeVarL];(*fをα変換した文全体.以下α変換によりfが変わっているかもしれないのでf1,f2を新たに取る*)
f1=StringTake[f,dot];(*最初のdotまでの（α変換された）文.元のf1と長さは同じ*)
f2=StringDrop[f,dot];(*最初のdot以降の（α変換された）文．元のf2と長さは同じ*)
f2=StringReplacePart[f2,L,{#,#}&/@freeX1];(*f2の中の自由変数x1の位置にLを代入*)
f1=StringReplace[f1,{"λ"~~_~~"."->"","λ"~~x_~~y__~~"."->"λ"~~y~~"."}];
Return[StringJoin[f1,f2]]
]

例

unitBeta[{"(λfx.(fx))","(λfx.(fx))"}](*第2項に自由変数がないからα変換されない．これは 1^1の計算*)

unitBeta[{"(λfx.(fx))","x"}](*1^1の計算の続き．この場合はα変換されてからβ変換．*)

[4]. stringBeta は「文」に対するβ変換

stringBetaは「文」から F = (λxy.M) N　などを最左簡約(Normal Order)で取り出し，unitBetaを使ってβ変換し, その結果をFと置き換えた文と，Fの前後の文をJointした文を出力する.

stringBeta[str_?(StringFreeQ[#,"(λ"]&)]:=str(*"(λ"が無い時はそのまま返す*)
stringBeta[str_String]:=Block[{s,βset,firstRedex,transformed,str1,str3,end},
s=deleteDuplicates[str];
firstRedex=makeRedexList[s][[1]];(*最左簡約*)
If[firstRedex=={},Goto[end]];
βset=StringTake[s,firstRedex];
transformed=unitBeta[βset];
str1=StringTake[s,UpTo[firstRedex[[1,1]]-1]];
str3=StringDrop[s,firstRedex[[2,2]]];
s=StringJoin[str1,transformed,str3];
Label[end];Return[deleteKakko[s]]
]

(*stringBeta[str_String]:=Block[{s,βset,firstRedex,transformed,str1,str3,end},
s=deleteDuplicates[str];
(*最左簡約*)
firstRedex=findLeftMostRedex[s];
If[firstRedex=={},Goto[end]];
βset=StringTake[s,firstRedex];
transformed=unitBeta[βset];
str1=StringTake[s,UpTo[firstRedex[[1,1]]-1]];
str3=StringDrop[s,firstRedex[[2,2]]];
s=StringJoin[str1,transformed,str3];
Label[end];Return[deleteKakko[s]]
]*)

例

stringBeta["(λfx.(fx))(λfx.(fx))"]
stringBeta[%]//deleteKakko(*α変換*)

[5]. マクロも使える．

初期設定ではnat(100までの自然数),true,false,or,and,not(真偽,論理演算子),add,sub,mul,succ,pred,leq,geq(和,差,積,次の数,前の数,以下,以上)がmacro2stringに定義されている．

macro2string は macro  から string を求めるAssociation

マクロはmacro2string に AssociateTo を使い自由に追加できる．＜＞で包んで定義する．下参照．

(*cn は church number*)
cn[0]="x";
cn[n_]:=StringReplace[cn[n-1],"x"->"(fx)"];
nat[n_]:="(λfx."<>cn[n]<>")";
natvalues=nat[#]&/@Range[0,100];(*100までの自然数の文字列の作成*)
natkeys="<"<>ToString[#]<>">"&/@Range[0,100];
macro2string=AssociationThread[natkeys,natvalues];

AssociateTo[macro2string,{"<true>"->"(λuv.u)","<false>"->"(λuv.v)"}];(*マクロの追加*)
AssociateTo[macro2string,{"<mul>"->"(λmn.λsz.m(ns)z)","<add>"->"(λmn.λsz.ms(nsz))","<power>"->"(λmn.nm)","<succ>"->"(λn.λsz.s(nsz))","<pred>"->"(λnfx.n(λgh.h(gf))(λu.x)(λu.u))","<sub>"->"(λmn.n<pred>m)"}];
AssociateTo[macro2string,{"<iszero>"->"(λn.n(λx.<false>)<true>)","<leq>"->"(λu.λv.<iszero>(<sub>uv))","<geq>"->"(λu.λv.<iszero>(<sub>vu))"}];
AssociateTo[macro2string,{"<and>"->"(λp.λq.p q p)","<or>"->"(λp.λq.p p q)","<not>"->"(λp.p<false><true>)"}];
AssociateTo[macro2string,{"<pair>"->"(λx.λy.λf.fxy)","<first>"->"(λp.p<true>)","<second>"->"(λp.p<false>)"}];
AssociateTo[macro2string,{"<Y>"->"(λg.(λx.g(xx))(λx.g(xx)))","<Z>"->"(λf.(λx.f(λy.xxy))(λx.f(λy.xxy)))","<G>"->"(λr.(λn.(<iszero>n)<1>(<mul>n(r(<pred>n)))) )",
"<factZ>"->"(λf.(λx.f(λy.xxy))(λx.f(λy.xxy)))(λg.λn.(λctf.ctf)((λn.n(λx.(λuv.v))(λuv.u)) n)(λfx.(fx))((λmn.λsz.m(ns)z)n(g((λnfx.n(λgh.h(gf))(λu.x)(λu.u))n))))","<factY>"->"(λf.(λx.f(xx))(λx.f(xx)))(λg.λn.(λctf.ctf)((λn.n(λx.(λuv.v))(λuv.u)) n)(λfx.(fx))((λmn.λsz.m(ns)z)n(g((λnfx.n(λgh.h(gf))(λu.x)(λu.u))n))))""<T>"->"(λr.λn.<iszero>n<1>(<add>n(r(<pred>n))))"}];

例

macro2string["<true>"]
macro2string["<false>"]
macro2string["<"<>ToString[#]<>">"]&/@Range[0,5](*church number*)

逆に string から定数 macro (nat, true,false) を求めるのが string2macro

countf[n_]:=Block[{afterperiod,f},
afterperiod=StringDrop[n,Last[StringPosition[n,"."]][[1]]];
f=StringCases[n,StartOfString~~"λ"~~x_->x];
StringCount[afterperiod,f]
]

string2macro[s_]:=Block[{n,zero,true,false},
n=StringCases[s,{"λ"~~f_~~x_~~"."~~{"("~~f_}..~~x_~~")"../;x≠f,"λ"~~f_~~x_~~"."~~f_~~{"("~~f_}..~~x_~~")"../;x≠f,
"λ"~~f_~~".(λ"~~x_~~"."~~{"("~~f_}..~~x_~~")"../;x≠f,"λ"~~f_~~".(λ"~~x_~~"."~~f_~~{"("~~f_}..~~x_~~")"../;x≠f,
"λ"~~f_~~".(λ"~~x_~~"."~~{"("~~f_}..~~"("~~x_~~")"../;x≠f,"λ"~~f_~~x_~~"."~~{"("~~f_}..~~"("~~x_~~")"../;x≠f}];
zero=StringCases[s,{"λ"~~f_~~x_~~"."~~"("~~x_~~")"/;x≠f,"λ"~~f_~~x_~~"."~~x_/;x≠f}];
true=StringCases[s,{"λ"~~f_~~x_~~".("~~f_~~")"/;x≠f,"λ"~~f_~~x_~~"."~~f_/;x≠f,
"λ"~~f_~~"("~~x_~~".("~~f_~~")"../;x≠f,"λ"~~f_~~".("~~x_~~"."~~f_~~")"../;x≠f}];
false=StringCases[s,{"λ"~~f_~~x_~~".("~~x_~~")"/;x≠f,"λ"~~f_~~x_~~"."~~x_/;x≠f,
"λ"~~f_~~"("~~x_~~".("~~x_~~")"../;x≠f,"λ"~~f_~~".("~~x_~~"."~~x_~~")"../;x≠f}];
Which[SameQ[true,{s}],"<true>",SameQ[zero,{s}],"<0>/<false>",SameQ[n,{s}],"<"<>ToString[countf[s]]<>">",
SameQ[false,{s}],"<false>",True,s]
]

[6].main command:  reduce[string], reduceList[string]

reduceList[string] で string を 簡約(α,β変換) した文のリストが出力される. reduce は最終結果のみ. 最大簡約回数は $maxReduction に入っていて 最初は100 に設定.

reduceは stringBetaを FixedPointを使って繰り返しているだけ

getNthResult[result_String,n_Integer] は, reduceList の出力のn番目を取り出す

(*左右の括弧の数のチェック*)
kakkoQ[s_String]:=StringCount[s,"("]==StringCount[s,")"];
(*マクロの展開*)
unitdecode[s_]:=Block[{anglesPos,decoded},
anglesPos=StringPosition[s,Shortest["<"~~___~~">"]];
decoded=macro2string[StringTake[s,#]]&/@anglesPos;
StringReplacePart[s,decoded,anglesPos]
]
decode[s_?(StringFreeQ[#,"<"]&)]:=s
decode[s_]:=NestWhileList[unitdecode,s,!StringFreeQ[#,"<"]&]

$maxReduction=100;(*max reduction times*)

reduceList[s_String?kakkoQ]:=Block[{input1,input2,input3,abbreviation,list},
input1=StringReplace[s,Whitespace->""];
input2=decode[input1]//StringReplace[#,Whitespace->""]&;(*decodeされていると Listになる*)
input3=If[SameQ[input1,input2],input1,Last[input2]];
list=FixedPointList[stringBeta,input3,$maxReduction]//Drop[#,-1]&;
abbreviation=string2macro[Last[list]];
If[UnsameQ[Last[list],abbreviation],AppendTo[list,abbreviation]];
list=If[UnsameQ[input1,input2],Join[input2,list//Drop[#,1]&],list];
StringJoin[Riffle[list,"\n⟶ "]]
]
reduceList[s_String]:=Print["Unbalanced brackets!"]

reduce[s_String?kakkoQ]:=Block[{input1,input2,input3,result,abbreviation},
input1=StringReplace[s,Whitespace->""];
input2=decode[input1]//StringReplace[#,Whitespace->""]&;(*decodeされていると Listになる*)
input3=If[SameQ[input1,input2],input1,Last[input2]];
result=FixedPoint[stringBeta,input3,$maxReduction];
abbreviation=string2macro[result]
]
reduce[s_String]:=Print["Unbalanced brackets!"]

getNthResult[result_String,n_Integer]:=Block[{pos,element},
pos=StringPosition[result,Shortest[{StartOfString~~___~~"⟶","⟶"~~___~~"⟶","⟶"~~___~~EndOfString}]];
element=If[n>0,StringTake[result,pos[[n]]],StringTake[result,pos[[n]]]];
Which[n==1,StringCases[element,x___~~"⟶"->x],n==-1,StringCases[element,"⟶"~~x___~~EndOfString->x],True,StringCases[element,"⟶ "~~x___~~"⟶"->x]]//First
]

メインコマンド使用例(reduceList&reduce)

reduceList["(λxy.(xyx))a b"]
reduceList["(λx.((λy.(xy))x))(ay)"]
reduceList["(λxyz.xz(yz))(λxy.x)(λxy.x)"]
reduceList["(λx.(xx))(λy.y)"]
reduceList["(λxy.(xyx))ab"]
reduceList["(λp.(p(λxy.x))) ((λp.(p(λxy.y))) (λx.(x(λy.(y a b)))(λz.(z c d))))"]
reduceList["<add><2><3>"]
reduceList["<mul><2><3>"]
reduceList["<power><2><3>"]
reduce["<power><2><3>"]

更なるマクロの使用例は 「マクロ編」 を御覧ください