我刚刚开始使用 Isabelle，在完成具体语义中的练习 3.3 时遇到类型统一错误：
定义替换函数
subst :: vname ⇒ aexp ⇒ aexp ⇒ aexp这样
subst x a e是将变量x的每次出现替换为e中的a的结果。例如：subst ''x'' (N 3) (Plus (V ''x'') (V ''y'')) = Plus (N 3) (V ''y'')
这是我到目前为止得到的：
theory Scratchpad
imports Main
begin
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"
datatype aexp = N int | V vname | Plus aexp aexp
fun subst :: "vname ⇒ aexp ⇒ aexp ⇒ aexp" where
"subst x (N a) (N e) = (N e)" |
"subst x (N a) (V e) = (if x=e then (N a) else (V e))" |
"subst x (N a) (Plus e1 e2) = Plus(subst(x (N a) e1) subst(x (N a) e2))"
end
当函数定义中的第三种情况被注释掉时，运行测试用例
value "subst ''x'' (N 3) (N 5)"
value "subst ''x'' (N 3) (V ''x'')"
分别产生(N 5)和(N 3)，所以我知道前两行工作正常。添加最后一行会导致错误
类型统一失败："_ ⇒ _"和"_ 列表"类型冲突
应用程序中的类型错误：运算符不是函数类型
运算符：x ：： 字符列表
操作数： N a ：： aexp
我不认为这是一个语法问题，尽管我还不完全确定不同类型的引号有什么用途（例如双引号与两个单引号）。从这个答案中，我相信 Isabelle 将x分配给行右侧的函数类型，这不是我想要的。
错误消息的实际含义（具体和一般），我该如何解决这个问题？
要回答有关引号的问题：Isabelle/HOL 中使用了两个单引号（更准确地说是其内部语法）来表示字符串文字。也就是说，通过''abc''，我们表示包含三个字符的字符串 a 、 b 和 c（如果您必须按字面意思输入它们，它将再次使用一些特殊语法）。另一方面，双引号主要用于将 Isar 语句（外部语法）与逻辑内的术语分开。因此，虽然''...''是术语语言的一部分，但"..."不是。
现在是错误消息。它告诉您您正在尝试使用列表x（类型 _ list ）作为函数（类型 _ => _ ）。为什么 Isabelle 认为您想将x用作函数？好吧，因为并列（即，将术语彼此相邻，用空格分隔）表示函数应用程序。因此，x (N a)被解释为将函数x应用于参数(N a)（就像f y将f应用于参数y一样）。为了给你的定义正确的含义，你必须在正确的位置使用括号。我想你在第三条中的意图是：
Plus (subst x (N a) e1) (subst x (N a) e2)
其中，我们有两个出现的函数subst应用于三个参数。（所以这毕竟是一个语法问题;)。
另一条评论。您对subst的实现可能更通用。照原样，subst 的第二个参数始终固定为某个数字a（因为您使用了构造函数 N ）。但是，如果您允许类型 aexp 的任意表达式，则一切应该正常工作。