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

Question

В модуле Poly есть 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 к некоторым x0 n+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 дополнительное время где-нибудь.Вы видите где?Есть две возможности.