Люди, участвующие в обмене стека CS , могли бы предоставить более глубокое понимание, но вот попытка.
Индуктивные типы данных определяются в исчислении конструкций с кодировкой Черча : тип данных является типом его функции сгиба. Самым основным примером являются натуральные числа, которые определяются следующим образом с использованием Coq-подобной записи:
nat := forall (T : Type), T -> (T -> T) -> T
Эта кодировка дает две вещи: (1) члены zero : nat и succ : nat -> nat для построения натуральных чисел и (2) оператор nat_rec для написания рекурсивных функций.
zero : nat
zero T x f := x
succ : nat -> nat
succ n T x f := f (n T x f)
nat_rec : forall T, T -> (T -> T) -> nat -> T
nat_rec T x f n := n T x f
Если мы представим F := nat_rec T x f для терминов x : T и f : T -> T, мы увидим, что справедливы следующие уравнения:
F zero = x
F (succ n) = f (F n)
Таким образом, nat_rec позволяет нам определить рекурсивные функции, указав возвращаемое значение x для базового случая и функцию f для обработки значения рекурсивного вызова. Обратите внимание, что это не позволяет нам определять произвольные рекурсивные функции на натуральных числах, а только те, которые выполняют рекурсивные вызовы предшественника своего аргумента. Разрешение произвольной рекурсии открыло бы дверь частичным функциям, что поставило бы под угрозу надежность исчисления.
Этот пример может быть обобщен на другие индуктивные типы данных. Например, мы можем определить тип списков натуральных чисел как тип их функции сгиба справа:
list_nat := forall T, T -> (nat -> T -> T) -> T