Pensieve header: Λ calculus as studied in Vietnam and on the way there.

bbCalclus.m is loaded only for comaprisons.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2013-05"];
<< ../2012-05/bbCalculus.m;
bbSimplify=Factor;
tha[u_,x_][β_B] := swapth[u,x][β];

f_∖key_ := DeleteCases[f, key -> _];
f_ ∖ keys_List := Fold[#1∖#2&, f, keys];

Alternate[expr_] := Expand[expr /. (s_Ts|s_Hs) :> Signature[s]Sort[s]];

tϵ[u_] := L[Hs[]Ts[],{}];
hϵ[x_] := L[Hs[]Ts[], {x->1}];
(SuperPlus[ρ])[u_,x_] := L[Ts[]Hs[] + ((Subscript[t, u])-1)Ts[u]Hs[x], {x->(Subscript[t, u])}];
(SuperMinus[ρ])[u_,x_] := L[Ts[]Hs[] + (((Subscript[t, u])^(-1))-1)Ts[u]Hs[x], {x->((Subscript[t, u])^(-1))}];
(SuperPlus[R])[a_,b_] := (SuperPlus[ρ])[a,b]hϵ[a]tϵ[b];
(SuperMinus[R])[a_,b_] := (SuperMinus[ρ])[a,b]hϵ[a]tϵ[b];

L /: L[λ1_,σ1_]L[λ2_,σ2_] := Module[{Hs1,Ts1,Hs2, Ts2},
L[
Expand[(λ1 /. {Ts->Ts1, Hs->Hs1})*(λ2 /. {Ts->Ts2, Hs->Hs2})] /. Ts1[ts1___]*Ts2[ts2___] :> Ts[ts1,ts2] /. 
Hs1[hs1___]*Hs2[hs2___] :> Hs[hs1,hs2],
Join[σ1,σ2] // Sort
] // Alternate
];

(SuperMinus[R])[1,2]

tm[u_,v_,w_][L[λ_,σ_]] := L[λ,σ] /. {
ts_Ts :> (ts /. {u->w, v->w}),
(Subscript[t, u])->(Subscript[t, w]), (Subscript[t, v])->(Subscript[t, w])
} // Alternate;

hm[x_,y_,z_][L[λ_,σ_]] := Module[
{σx=x/.σ, σy=y/.σ},
L[
(λ /. hs_Hs /; MemberQ[hs, y] :> σx*hs) /. hs_Hs :> (hs /. {x->z, y->z}),
Union[σ∖{x,y}, {z-> σx*σy}]
] // Alternate
]

tha[u_,x_][L[λ_,σ_]] := Module[
{σx=x/.σ},
L[Plus[
λ /. ts_Ts /; MemberQ[ts, u] :> σx*ts,
Expand[λ /. {
ts_Ts :> If[FreeQ[ts, u], 0, (((-1))^(Position[ts,u][[1,1]]))*DeleteCases[ts,u]],
hs_Hs :> If[FreeQ[hs, x], 0, (((-1))^(Position[hs,x][[1,1]]))*DeleteCases[hs,x]]
}]
],σ]  // Alternate
]

dm[a_,b_,c_][Λ_L] := Λ// tha[a,b] // tm[a,b,c] // hm[a,b,c];

B[L[λ_,σ_]] := bbCollect[B[
Coefficient[λ, Hs[]Ts[]] /. (Subscript[t, u_]) :> (Subscript[T, u]),
Plus @@ (σ /. (x_ -> σx_) :> h[x](σx /. (Subscript[t, u_]) :> (Subscript[T, u]))),
λ /. {Ts[u_] :> t[u], Hs[x_] :> h[x]} /. {_Ts -> 0, _Hs ->0} /. (Subscript[t, u_]) :> (Subscript[T, u])
]];