Церковные цифры

Question

В модуле Поли есть 4 упражнения, связанные с церковными цифрами:

Definition cnat := forall X : Type, (X -> X) -> X -> X.

Насколько я понимаю, cnat - это функция, которая принимает функцию f(x), это аргумент x и возвращает значение этого аргумента: f(x).

Тогда есть 4 примера для 0, 1, 2 и 3, представленные в церковной записи.

Но как это решить? Я понимаю, что мы должны применить функцию еще раз. Значение, возвращаемое cnat, будет аргументом. Но как это закодировать? Использовать рекурсию?

Definition succ (n : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Обновить

Я попробовал это:

Definition succ (n : cnat) : cnat :=
match n with
| zero => one
| X f x => X f f(x) <- ?

Answer 1

Помните, что церковное число - это функция двух аргументов (или трех, если вы также учитываете тип). Аргументы являются функцией f и начальное значение x0, Церковная цифра применяется f в x0 некоторое количество раз. Four f x0 будет соответствовать f (f (f (f x0))) а также Zero f x0 будет игнорировать f и просто быть x0,

Для преемника nпомни что n будет применять любую функцию f для тебя n раз, так что если ваша задача создать функцию, применяет некоторые f на некоторых x0n+1 просто оставьте большую часть работы церковной цифре n, дав ей свой f а также x0, а затем завершить с еще одним применением f к результату, возвращенному n,

Вам не понадобится match потому что функции не являются индуктивными типами данных, которые могут быть проанализированы на...

Answer 2

Вы можете написать Definition за succ следующим образом:

Definition succ (n : cnat) : cnat :=
    fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

Answer 3

Насколько я понимаю, cnat - это функция, которая принимает функцию f(x), это аргумент x и возвращает значение этого аргумента: f(x).

Обратите внимание, что cnat само по себе не является функцией. Вместо, cnat тип всех таких функций. Также обратите внимание, что элементы cnat принимать X в качестве аргумента, а также. Это поможет сохранить определение cnat в уме.

Definition succ (n: cnat): cnat.
Proof.
  unfold cnat in *. (* This changes `cnat` with its definition everywhere *)
  intros X f x.

После этого наша цель просто X, и у нас есть n : forall X : Type, (X -> X) -> X -> X, X, f а также x как помещения.

Если мы подали заявку n в X, f а также x (как n X f x), мы бы получили элемент X, но это не совсем то, что мы хотим, так как конечный результат будет просто n снова. Вместо этого нам нужно применить f дополнительное время где-то. Вы видите где? Есть две возможности.