是否可以定义存储与参数具有相同数据类型的 lambda 函数的数据类型？

Question

我正在尝试创建一个包含 lambda 函数的数据类型，该函数采用与参数相同的数据类型。

这是一个例子：

datatype id = n_1 | n_2

type_synonym entry = "(id * (entry list ⇒ nat))"
type_synonym myList = "entry list"

fun ivalue :: "myList ⇒ nat"
  where
    "ivalue [] = 0" |
    "ivalue (x # xs) = snd x (x xs)"

fun search :: "myList ⇒ id ⇒ myList"
  where
    "search [] t = []" |
    "search (x # xs) t = (if fst x = t then (x # xs) else search xs t)"

definition my_list :: "myList"
  where
    "my_list = [(n_1, %p.(42::nat)),
                (n_2, %p.(ivalue (search p n_1)) + 6)]"

代码的想法是拥有带有 ID 和表达式的元组列表。该表达式由一个 lambda 函数实现，该函数本身可以获取相同格式的列表。 search 和 ivalue 函数允许引用表达式中的其他条目。计算my_list 中所有表达式的算法的预期结果是[(n_1, 42), (n_2, 48)]。

entry 的定义显然是错误的，但希望能说明我试图实现的目标。有没有办法创建这样的数据类型？

Answer 1

这是不可能的，因为它在数学上是不一致的。简而言之，这样的数据类型太大而无法放入集合中。 （如果是这样，人们可以很容易地从这种类型的能量集构造一个注入到自身中）

您可以找到更详细的说明，例如here.

如果您要存储的函数具有受限域（例如，有限域或可数域），则可以使其工作。我会天真地认为有限映射会起作用：

datatype entry = Entry id "(entry list, nat) fmap"

但显然不是。这是由于一个深刻的逻辑问题还是仅仅因为 fmap 没有正确设置以支持这一点，我不确定。我怀疑是后者，因为以下类似的事情确实有效：

datatype entry = Entry id "(entry list × nat) fset"

有限的地图对你来说就足够了吗？