User:I am islptng/Lambda Calculus in Polynomix

$$ Lambda calculus implementation, operating on a flat token stream

(str>str\(~`0123456789'-<)!@.+.-*.!!str)#\Tokenize
(tk>
    []#\res [0]#\stk []#\abst 0|#\inlam
    tk\(i>
        i=`('?(stk#+[0]
        i=`)' {
            stk/\1?(abst#/(\;,(stk/\1-)))
            stk#/(\;,\1)
        }
        i=`\' 1|#inlam
        i=`.' 0|#inlam
            inlam?({
                abst#+[i]
                stk/((+1)\1)
            }
                i~abst-?(res#+[i])
    )))!;
    res
)#\GetFreeVars
(tk>
    []#\res 0|#\inlam
    tk\(i>
        i=`\'?(1|#inlam
        i=`.'  0|#inlam
            inlam?(res#+[i])
        )
    )!;
    res-[`(' `)']
)#\GetAbstractions
(var env>
    var/|.(~`0123456789')/#var
    var~env-?(var@)
    1#\i
    var+(i*.)~env@(i#+1)
    var+(i*.)
)#\FreshVar
(tk>
    1#\cnt
    {
        c=`('?(cnt#+1)
        c=`)'?(cnt#-1)
        cnt=0?(tk-(i+1)@)
    }@(1#\i 1 tk/i#\c i#+1)
)#\TakeParen
(tk> TakeParen#;
    tk/0=`\'?(tk,[]@)
    tk/0=`('-?(tk-1@)
    tk TakeParen!#([\;tk!!\;],\left)
    tk/0=`('@{
        tk TakeParen!#([\;tk!!\;],\left2)
        left2+left#left
    }
    tk/0=`\'?(tk,left
    {
        tk-1#(tk,\left2)
        tk,(left2+left)
    })
)#\TakeExprF
(tk> TakeParen#;
    tk/0=`\'?(tk,[]@)
    tk/0=`('-?(tk-1@)
    tk TakeParen!
)#\TakeExprA
(tk>
    tk/0=`\'-?(\;,tk@)
    tk-(tk%`.'/0)#\([\;abst!!],[\;body!!])
    abst<=1?(abst/0,body@)
    abst#[abst\rest!!]
    abst,(`\',+rest+[`.']+body)
)#\ParseLambda
(tk var tar>
    []#\res 1#\pars 0#\shadl 0|#\inlam
    tk\(i>
        i=`('?({pars#+1 res#+[i]}
        i=`)' {
            shadl=pars?(0#shadl)
            pars#-1
            res#+[i]
        }
        i=`\'{1|#inlam res#+[i]}
        i=`.'{0|#inlam res#+[i]}
        i=var res#+(shadl?(
            [i]
            inlam?({pars#shadl [i]} tar)
        ))
        res#+[i]
    ))!;
    res
)#\ReplaceExpr
(tk> GetFreeVars#; GetAbstractions#; FreshVar#; TakeExprF#; TakeExprA#; ParseLambda#; ReplaceExpr#;
    tk TakeExprF!#\(func,rest)
    rest|-?(\;@) $$ Irreducible
    rest TakeExprA!#\(arg,rest)
    func ParseLambda!#\(var,body)
    var=\;?(\;@) $$ Irreducible
    body GetAbstractions!#\abst
    abst&arg#\alphas
    arg+(func GetFreeVars!)-[`('`)'`\'`.']#\fv
    alphas\(i>
        body#*(i,;i FreshVar!fv,)
    )!;
    body ReplaceExpr!(var arg)#\res
    res/0=`\'?(`(',+res+[`)']#res)
    res+rest
)#\BetaFront

$$ Entry Point
(expr> TakeExprA#; BetaFront#;
    expr(tk> TakeExprA#; BetaFront#;
        tk BetaFront!#\res
        res=\;-?(res@)
        tk TakeExprA!#\(irred,rest)
        irred TakeExprF!#(irred,\rest2)
        rest2+rest#rest
        irred/0=`\'?{
            irred ParseLambda!#\(var,body)
            body\.#res
            res=\;-?(rest?(
                [`('`\'var`.']+res+[`)']+rest@;
                [`\'var`.']+res@
            ))
        }
        rest@{
            rest TakeExprA!#(\test,rest)
            test\.#res
            res=\;?(
                irred#+test
            {
                res<=1-?(`(',+res+[`)']#res)
                irred+res+rest@
            })
        }
    \;)!#\res
    res=\;?(expr res*([`.'`\'][]))
)#\BetaReduce

`(\fx.f(f(x)))(\fx.f(f(x)))' #\ src
src Tokenize! ~ (x>x BetaReduce!#\res res=>.;"\n>.;"\n>.;res)\;