lambda-calculus 中 2 个列表的串联

Question

我已经定义了多态列表的类型及其构造函数，现在尝试编写一个连接 2 个列表的函数，但我的函数 concat 不起作用

Definition listA A :Set :=
    forall T :Set, T -> (A -> T -> T) -> T.
    
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).
Definition concat (A :Set ) (a b:listA A): listA A :=
    a A b ( pcons A a b).

我得到函数 concat

的错误

In environment
A : Set
a : listeA A
b : listeA A
The term "b" has type "listeA A" while it is expected to have type "A".

Answer 1

你的函数有两个问题：首先，你使用 a 构建一些 listA A 而不是一些 A，所以它的第一个参数应该是 listA A而不是 A。其次，它的第三个参数也不正确：在 cons 的情况下，你只是想再次重用 cons，而不是使用 b，所以第三个参数应该是 pcons A而不是 pcons A a b.

最后，你得到

Definition concat (A :Set) (a b:listA A): listA A :=
    a (listA A) b (pcons A).

如果你想测试它并说服自己它做的是正确的，你可能想玩一下


Definition tolist (A : Set) (l : listA A) : list A :=
  l (list A) nil cons.

Fixpoint fromlist (A : Set) (l : list A) : listA A :=
  match l with
  | nil => pnil A
  | cons h t => pcons A h (fromlist A t)
  end.

从您的命令式编码转换为通常的数据类型并返回。例如，你可以做

Eval compute in tolist nat (concat nat (fromlist nat [0 ; 1]) (fromlist nat [2;3])).

看到结果确实是[0;1;2;3].

lambda-calculus 中 2 个列表的串联

Concatenation of 2 lists in lambda-calculus

coq

lambda-calculus

coqide