伊莎贝尔类型 unification/inference 错误

Question

我刚刚开始使用 Isabelle，在 Concrete Semantics:

中完成练习 3.3 时遇到类型统一错误

Define a substitution function
subst :: vname ⇒ aexp ⇒ aexp ⇒ aexp
such that subst x a e is the result of replacing every occurrence of variable x by a in e. For example:
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)，所以我知道前两行工作正常。添加最后一行会导致错误

Type unification failed: Clash of types "_ ⇒ _" and "_ list"

Type error in application: operator not of function type

Operator: x :: char list
Operand: N a :: aexp

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

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

Answer 1

回答你关于引号的问题：Isabelle/HOL（更准确地说是它的内部语法）中使用了两个单引号来表示字符串文字。也就是说，我们用 ''abc'' 表示包含三个字符 a、b 和 c 的字符串（如果您必须按字面意思输入它们，这将再次使用一些特殊语法).另一方面，双引号主要用于将 Isar 语句（外部语法）与逻辑内部的术语分开。因此，虽然 ''...'' 是术语语言的一部分，但 "..." 不是。

现在查看错误消息。它告诉您您正在尝试将列表 x（类型 _ list）用作函数（类型 _ => _）。为什么 Isabelle 认为您想使用 x 作为函数？好吧，因为并列（即，将术语并排书写，用白色 space 分隔）表示 函数应用 。因此 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.

类型的任意表达式，一切都应该正常工作

伊莎贝尔类型 unification/inference 错误

Isabelle type unification/inference error

isabelle