<p>The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit.  The encoding simply presents you with the results of recursion for all immediate subdata.  Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.</p>

The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit. The encoding simply presents you with the results of recursion for all immediate subdata. Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.

<p>The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit.&nbsp; The encoding simply presents you with the results of recursion for all immediate subdata.&nbsp; Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.</p>

The Mendler encoding and the problem of explicit recursion

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share The Mendler encoding and the problem of explicit recursion

Sign up to save your podcasts

The Mendler encoding and the problem of explicit recursion

The Mendler encoding and the problem of explicit recursion