Isabelle 类型统一/推理错误

Question

我刚开始使用 Isabelle，在完成 Concrete Semantics 的练习 3.3 时遇到类型统一错误：

定义一个替换函数

subst :: vname ⇒ aexp ⇒ aexp ⇒ aexp

使得subst x a e 是在e 中将变量x 替换为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

当函数定义中的第三个case被注释掉时，运行测试用例

value "subst ''x'' (N 3) (N 5)"
value "subst ''x'' (N 3) (V ''x'')"

分别产生(N 5) 和(N 3)，所以我知道前两行工作正常。添加最后一行导致错误

类型统一失败：类型“_ ⇒ _”和“_ list”的冲突

应用程序中的类型错误：运算符不是函数类型

运算符：x :: 字符列表
操作数：N a :: aexp

我认为这不是语法问题，尽管我还不能完全确定不同类型的引号的用途（例如双引号与两个单引号）。从this answer，我相信Isabelle 将x 指定为行右侧的函数类型，这不是我想要的。

错误消息的实际含义是什么（具体和一般），我该如何解决这个问题？

Answer 1

回答关于引号的问题：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 类型的任意表达式，那么一切都应该正常工作。