Start / Iowa Type Theory Commute / The mendler encoding and the problem of explicit recursion

Iowa Type Theory Commute

The Mendler encoding and the problem of explicit recursion

11 min • 25 februari 2020

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.

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

Krivine's Proof of FD, Using Intersection Types

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min

Podcastbild

00:00 -00:00

Podcastbild

00:00 -00:00