Lambda calculus is a system of computation based on single-argument functions; everything in it is such a function. Due to this functional nature, juxtaposition is commonly used to denote function application, grouped from left to right. For example, \$(f g) h=f g h\$ denotes what would conventionally be written \$(f(g))(h)=f(g)(h)\$.
Church numerals are a way of encoding the nonnegative integers in this system. They are defined as follows:
\$\begin{align*}
\overparen{\underparen0} f &= \operatorname{id}\\
\overparen{\underparen 1} f &= f\circ\left(\overparen{\underparen 0} f\right)=f\\
\overparen{\underparen 2} f &= f\circ\left(\overparen{\underparen 1} f\right)=f\circ f\\
\vdots\\
\overparen{\underparen n} f &= f\circ\left(\overparen{\underparen{n-1}} f\right)\\
&=\underbrace{f\circ\cdots\circ f}_n,
\end{align*}\$
where \$\circ\$ denotes function composition. In other words, the Church numeral \$\overparen{\underparen n}\$ can be seen as a unary operator on a function \$f\$ that nests that function \$n\$ times.
From here, we can define a binary operator (with two curried arguments) that performs addition on two Church numerals:
\$\begin{align*}
\operatorname{add} \overparen{\underparen a} \overparen{\underparen b} f&= \overparen{\underparen{a+b}} f\\
&= \left(\overparen{\underparen a} f\right)\circ\left(\overparen{\underparen b} f\right).
\end{align*}\$
That is, we nest \$f\$ \$b\$ times, then another \$a\$ times.
By definition, \$\operatorname{add} \overparen{\underparen a}\$ is a unary operator that, when applied to another Church numeral \$\overparen{\underparen b}\$, results in \$\overparen{\underparen{a+b}}\$. But what happens when we reverse the order, i.e. attempt to evaluate \$\overparen{\underparen a}\operatorname{add}\$? This resulting function has arity \$a+1\$, needed to expand out all the \$\operatorname{add}\$s in \$\underbrace{\operatorname{add}\circ\cdots\circ\operatorname{add}}_a\$.
Task
Given (optionally) an integer \$a\ge0\$, and another \$a+1\$ integers \$x_0,x_1,...,x_a\ge0\$, compute the integer \$n\$ such that \$\overparen{\underparen n}=\overparen{\underparen a} \operatorname{add} \overparen{\underparen{x_0}} \overparen{\underparen{x_1}}...\overparen{\underparen{x_a}}\$.
You probably will also need to know the multiplication and exponentiation rules:
\$\begin{align*}
\overparen{\underparen{a\times b}} f&=\overparen{\underparen a} \left(\overparen{\underparen b} f\right)=\left(\overparen{\underparen a}\circ\overparen{\underparen b}\right)f\\
\overparen{\underparen{a^b}} f &= \overparen{\underparen b} \overparen{\underparen a} f.
\end{align*}\$
Example
Take \$\overparen{\underparen 2} \operatorname{add} \overparen{\underparen 3} \overparen{\underparen 4} \overparen{\underparen 5}\$:
\$\begin{align*}
\overparen{\underparen 2}\operatorname{add}\overparen{\underparen 3} \overparen{\underparen 4} \overparen{\underparen 5}&=(\operatorname{add}\circ\operatorname{add})\overparen{\underparen 3} \overparen{\underparen 4} \overparen{\underparen 5}\\
&=\operatorname{add}\left(\operatorname{add}\overparen{\underparen 3}\right)\overparen{\underparen4} \overparen{\underparen5}\\
&=\left(\operatorname{add}\overparen{\underparen 3} \overparen{\underparen 5}\right)\circ\left(\overparen{\underparen 4} \overparen{\underparen 5}\right)\\
&=\overparen{\underparen 8}\circ\overparen{\underparen{5^4}}\\
&=\overparen{\underparen{5000}}
\end{align*}\$
Test cases
a x result
0 9 9
1 2,2 4
2 2,2,2 16
2 3,4,5 5000
2 7,1,8 120
3 1,4,1,5 30
3 2,2,2,2 4608
3 2,3,2,4 281483566645248
3 2,3,4,5 46816763546921983271558494138586765699150233560665204265260447046330870022747987917186358264118274034904607309686036259640294533629299381491887223549021168193900726091626431227545285067292990532905605505220592021942138671875
3 3,3,3,3 3381391913524056622394950585702085919090384901526970
4 2,2,2,2,2 120931970555052596705072928520380169054816261098595838432302087385002992736397576837231683301028432720518046696373830535021607930239430799199583347578199821829289137706033163667583538222249294723965149394901055238385680714904064687557155696189886711792068894677901980746714312178102663014498888837258109481646328187118208967028905569794977286118749919370644924079770214106530314724967825243764408114857106379963213188939126825992308882127905810306415158057997152747438230999039420121058243052691828798875998809865692983579259379718938170860244860482142976716892728044185832972278254093547581276129155886886086258355786711680193754189526351391221273418768272112491370597004152057820972058642174713955967404663467723362969481339278834627772126542657434779627861684834294203455419942997830922805201204107013187024101622800974572717408060065235993384198407691177770220323856866020553151446293957513282729090810520040166215232478427409757129336799823635731192497346452409939098243738098803206142762368603693303505732137119043739898807303126822830794424748280315330250324436290184499770851474706427973859450612731909450625705188122632367615184044521656851538649088840328591879043950831910516712687721046964100635071310295009799499919213218249505904439261442688728313586685099505945191069266179018225279933007599239168
6 Answers 6
Flurry, 28 bytes
({}){{}{}}[{}{<><<>(){}>}]{}
A language based on untyped lambda calculus is certainly the right tool here :)
Takes input in the order of xa xa-1 ... x1 x0 a
, and evaluates to the Church value of the required expression.
({}) pop a; evaluate to a; push back a
{{}{}} \x. x (pop), which takes a function and applies one item from stack
a (\x. x (pop)) [...] evaluates to [...] x0 x1 ... xa-1
[{} the expression (a add)
{<><<>(){}>} add = \x. S (S . K . x)
]
so far, the result is (a add x0 x1 ... xa-1)
{} finally, pop xa and apply to the above
Test script:
Compare-Object (.\Flurry.exe -nin src.txt 9 0) 9
Compare-Object (.\Flurry.exe -nin src.txt 2 2 1) 4
Compare-Object (.\Flurry.exe -nin src.txt 2 2 2 2) 16
Compare-Object (.\Flurry.exe -nin src.txt 5 4 3 2) 5000
Compare-Object (.\Flurry.exe -nin src.txt 8 1 7 2) 120
Compare-Object (.\Flurry.exe -nin src.txt 5 1 4 1 3) 30
Compare-Object (.\Flurry.exe -nin src.txt 2 2 2 1 3) 4352
Compare-Object (.\Flurry.exe -nin src.txt 2 2 2 0 3) 4096
Compare-Object (.\Flurry.exe -nin src.txt 2 2 2 2 3) 4608
Haskell, 54 bytes
x#y|(a,b)<-foldl(\(a,b)c->(c^b,(c^b)^a))(0,1)y=(x+a)*b
Takes input as \$x_0 \# [x_1,\dots,x_a]\$.
Abusing the notation, we have:
\0ドル \operatorname{add} x_0 = x_0 = (x_0 + 0) \times 1\$.
If we have
\$(n-1) \operatorname{add} x_0 \cdots x_{n-1} = (x_0 + a_{n-1}) \times b_{n-1}\$,
then:
\$\begin{align} n \operatorname{add} x_0 \cdots x_n &= (n-1) \operatorname{add} (\operatorname{add} x_0) x_1 \cdots x_{n-1} x_n \\ &= (((\operatorname{add} x_0) + a_{n-1}) \times b_{n-1}) x_n \\ &= ((\operatorname{add} (\operatorname{add} x_0) a_{n-1}) \circ b_{n-1}) x_n \\ &= \operatorname{add} (\operatorname{add} x_0) a_{n-1} (b_{n-1} x_n) \\ &= (\operatorname{add} x_0 (b_{n-1} x_n)) \circ (a_{n-1} (b_{n-1} x_n)) \\ &= (x_0 + {x_n}^{b_{n-1}}) \times ({x_n}^{b_{n-1}})^{a_{n-1}} \\ &= (x_0 + a_n) \times b_n \end{align} \$
where:
\$a_n = {x_n}^{b_{n-1}}, b_n = ({x_n}^{b_{n-1}})^{a_{n-1}}\$.
PARI/GP, 47 bytes
x->[[a,b]=[t=c^b,t^a]|c<-x[^b=!a=0]];(x[1]+a)*b
A port of my Haskell answer. Takes input as \$[x_0,x_1,\dots,x_n]\$.
Lambda calculus, 51 characters (or 73 bits)
The function takes two arguments (in curried form as usual): the first argument is a
as a Church numeral, and the second argument is a list of Church numerals.
\a\l l(\h\t\f t(f h))(\f f)(a(\m\n\f\x m f(n f x)))
Or in the binary lambda calculus encoding:
0000010101100000000111001101110001001110000000000101111101100101111011010
In lambda calculus, the standard representation of a list is: e.g. the list [a, b, c] is represented by \$\lambda x . \lambda y . x~a~(x~b~(x~c~y))\$. (As a mnemonic, I like to think of the case where \$x = \mathrm{cons}\$ and \$y = \mathrm{nil}\$.) In other words, in lambda calculus, a list is its "fold-right" operation.
Now, if we have a list \$l\$, the expression \$l ~ (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ (\lambda f . f)\$ builds up an "apply" operation. For example, in the case \$l = [a, b, c]\$, it evaluates to \$\lambda f . f ~ a ~ b ~ c\$. (To see this, for example: $$ [a, b, c] (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ (\lambda f . f) = \\ (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ a ~ ([b, c] (\lambda h . \lambda t. t ~ (f ~ h)) ~ (\lambda f . f)) = \\ (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ a ~ (\lambda f . f ~ b ~ c) = \\ \lambda f . ((\lambda f . f ~ b ~ c) (f ~ a)) = \\ \lambda f . f ~ a ~ b ~ c$$ where from the second line to the third we applied an inductive hypothesis on the case \$l = [b, c]\$. For the base case, the empty list is \$l = [] = \lambda x . \lambda y . y\$, so \$l ~ (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ (\lambda f . f) = \lambda f . f\$. Alternatively, you can see this as a special case of how in general you would write a fold-left operation on lists in terms of the fold-right operation.)
From here, what we want is simply: \$\lambda a . \lambda l . \mathrm{apply} ~ (a ~ \mathrm{add}) ~ l\$. Substituting \$\mathrm{apply} = \lambda f . \lambda l . l (\lambda h . \lambda t . \lambda f . t ~ (f ~ h)) ~ (\lambda f . f) ~ f\$, and \$\mathrm{add} = \lambda m . \lambda n . \lambda f . \lambda x . m ~ f ~ (n ~ f ~ x)\$ gives the final expression above.
-
\$\begingroup\$ Since taking reversed list as input is allowed,
\a l. l (\x y. y x) (a (B add) I)
should also work. \$\endgroup\$Bubbler– Bubbler2022年07月25日 04:31:17 +00:00Commented Jul 25, 2022 at 4:31
JavaScript (Node.js), (削除) 65 (削除ここまで) 56 bytes
Saved 7 bytes thanks to @tsh
This is really just a port of alephalpha's algorithm.
Expects (n)(x)
, where x
is an array of BigInts.
x=>x[x.map((v,i)=>[a,b]=i?[v**=b,v**a]:[0n,1n]),0]*b+a*b
Or 54 bytes without BigInts:
x=>x[x.map((v,i)=>[a,b]=i?[v**=b,v**a]:[0,1]),0]*b+a*b
-
1
Binary Lambda caclulus, 39 bits (< 5 bytes).
In lambda calculus with church numerals, that function is simply λa. a add = λa. a(λmλnλfλx. m f (n f x)), with blc encoding 000110000000000101111101100101111011010), since eta expansion handles all the additional arguments.
x
in reverse order? \$\endgroup\$