解释后的语言环境继承

Question

我试图了解“继承”在语言环境/解释级别上如何工作。我有一个抽象语言环境 (locA)，其中定义了一个方法 (g)。我有一个具体的语言环境（locB），它是抽象语言环境的实例/模型。有没有一种方法可以使用

g

方法，让我不会收到“类型统一”错误？

下面是我想要实现的目标的玩具示例

theory InstOverwrite

imports Main
begin

locale locA = 
  fixes f :: "'a ⇒ 'b"
begin

definition g :: "'a set ⇒ 'b set" where 
  "g X = f`X"
end

locale locB = 
  fixes fb :: "nat ⇒ nat"
  assumes fb_def: "fb n = n*2"
begin

interpretation locA
  apply unfold_locales
  done
end

context locB
begin
definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ locA.g X}"
end

end

毫不奇怪，我收到以下错误：

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

Type error in application: incompatible operand type

Operator:  locA.g :: (??'a ⇒ ??'b) ⇒ ??'a set ⇒ ??'b set
Operand:   X :: nat set

Answer 1

快速修复

在您的代码中，您尚未实际连接这两个区域设置。

locA.g

存在于语言环境“外部”，因为必须为其提供

f :: "'a ⇒ 'b"

才能使用。这就是伊莎贝尔试图通过强调

Operator:  locA.g :: (??'a ⇒ ??'b) ⇒ ??'a set ⇒ ??'b set

来表达的意思。因此，为了让类型检查器在这里满意，您需要明确指出

fb

应该在函数应用程序中充当

f

。

definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ locA.g fb X}"

（唯一的区别是写

locA.g fb X

而不是

locA.g X

。）

提供参数给

interpretation

从您对问题的描述中，我了解到您希望

interpretation locA

能够负责建立此连接。事实并非如此。

要建立

f := fb

的实例化，您需要为解释提供参数。以下内容可行：

interpretation locA fb .

definition fx :: "nat set ⇒ nat set" where
  "fx X = {n+1 | n::nat. n ∈ g X}"

（注意现在是

g X

而不是

locA.g fb X

！）

也许更

sublocale

？

我方便地从示例脚本中删除了结束/开始上下文。原因是上下文跳转会破坏解释。如果您希望跨上下文保持连接，则

sublocale

关键字更合适：

sublocale "locA" fb .
end (* of locale context locB *)

(* somewhere else we may add to the locale again: *)

definition (in locB) fy :: "nat set ⇒ nat set" where
  "fy X = {n+1 | n::nat. n ∈ g X}"

有关语言环境继承的更多说明

根据您实际想要做什么，更不同的表述可能更有意义。我认为列表只是提供一些最小示例的方式。

对于遇到这个问题的人，我想指出，这里的语言环境继承情况可以通过以下两种方法之一更方便地表达：

A) 使

locB

延伸

locA

:

以下内容将直接对两个语言环境使用相同的

f

并仅添加定义假设：

locale locB = 
  locA f for f :: "nat ⇒ nat" +
  assumes f_def: "f n = n*2"

B) 让

locB

指定

locA

definition fb :: "nat ⇒ nat" where "fb n ≡ n * 2"

locale locB = 
  locA fb