是否可以定义存储与参数具有相同数据类型的 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

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

您可以找到更详细的解释，例如.

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

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

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

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

有限地图对您来说是否足够？

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

Can a data type be defined which stores a lambda function that has the same data type as parameter?

lambda

isabelle