Church 平等编码的递归
Recursion for Church encoding of equality
对于正整数的Church编码N
,可以定义一个递归原理nat_rec
:
Definition N : Type :=
forall (X:Type), X->(X->X)->X.
Definition nat_rec (z:N)(s:N->N)(n:N) : N :=
n N z s.
下面Church编码equal
等式的递归原理equal_rec
是什么?
Definition equal (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.
Definition equal_rec (* ... *)
和自然数的情况一样,递归原理只是一个eta展开:
Definition equal (A:Type) (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.
Definition equal_rec (A:Type) (x y : A) (e : equal x y) (P : A -> Type) : P x -> P y :=
e P.
对于正整数的Church编码N
,可以定义一个递归原理nat_rec
:
Definition N : Type :=
forall (X:Type), X->(X->X)->X.
Definition nat_rec (z:N)(s:N->N)(n:N) : N :=
n N z s.
下面Church编码equal
等式的递归原理equal_rec
是什么?
Definition equal (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.
Definition equal_rec (* ... *)
和自然数的情况一样,递归原理只是一个eta展开:
Definition equal (A:Type) (x:A) : A->Type :=
fun x' => forall (P:A->Type), P x -> P x'.
Definition equal_rec (A:Type) (x y : A) (e : equal x y) (P : A -> Type) : P x -> P y :=
e P.