lambda-calculus 列表中的元素数？

Question

我正在 coq 中编写多态列表，我已将类型定义为

Definition listA A :Set :=
    forall T :Set, T -> (A -> T -> T) -> T.
(* empty list*)
Definition pnil (A :Set) : listA A := 
      fun T: Set => fun (x : T ) => fun (c : A -> T -> T) => x.
     
Definition pcons (A :Set): A -> (listA A) -> (listA A):=
    fun (a : A) (q : listA A) => fun T : Set => fun (x : T ) => fun (c : A -> T -> T) => c a (q T x c).

但是当我尝试计算列表中有多少元素时出现错误：

Unknown constructor: pcons.

这是我写的计算元素的代码。

Fixpoint nb_elements (A :Set ) (l :listA A): nat :=
    match l with 
        | pnil => 0
        |pcons A e t => 1 + (nb_elements A t)
    end.

Answer 1

您对 listA 的定义是 System F 中列表的编码，即多态 lambda 演算。要使用这些列表，您需要将它们用作函数而不是求助于 Coq 的 match 语句。例如：

Definition nb_elements (A : Set) (l : listA A) : nat :=
  l nat 0 (fun (x : A) (count : nat) => S count).

直觉上，listA 的第二个参数指定在基本情况下 return 的内容，而第三个参数指定对 non-empty 列表执行的操作。这里，如果列表为空，则元素个数为0。如果列表为non-empty，假设我们已经计算出其尾部的元素个数，我们称之为count。然后，为了计算整个列表的元素数量，我们只需要在 count.

上加一

实际上，在 Coq 中很少使用 listA 等编码数据类型。通常，我们使用归纳定义的类型，这允许我们使用 match 语句。这是使用归纳列表类型的示例版本：

Inductive list A : Set :=
| nil : list A
| cons : A -> list A -> list A.
Arguments nil {A}.
Arguments cons {A}.

Fixpoint nb_elements (A : Set) (l : list A) : nat :=
  match l with
  | nil => 0
  | cons x l' => S (nb_elements A l')
  end.

lambda-calculus 列表中的元素数？

Number of element in a list in lambd-calculus?

lambda-calculus

coq