1

我正在使用 HOL-Z 中的数学工具包来释放一些 Isabelle 谓词。具体来说，我使用部分函数定义来定义我正在编写的 Z 规范中的一些关系，在其中我将模式转换为规范语句，以便我可以生成简单的 HOL 谓词。

来自 HOL-Z 工具包的定义

type_synonym      ('a,'b) lts = "('a*'b) set"     (infixr "<=>" 20)

  prodZ       ::"['a set,'b set] => ('a <=> 'b) "        ("_ %x _"  [81,80] 80)
"a %x b"        == "a <*> b"

rel           ::"['a set, 'b set] => ('a <=> 'b) set"    ("_ <--> _"   [54,53] 53)
rel_def       : "A <--> B    == Pow (A %x B)"

partial_func  ::"['a set,'b set] => ('a <=> 'b) set"     ("_ -|-> _"   [54,53] 53)
partial_func_def  : "S -|-> R    == 
    {f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f  --> (y1=y2))}"

rel_appl      :: "['a<=>'b,'a] => 'b"    ("_ %^ _"  [90,91] 90)
rel_appl_def  :  "R %^ x       == (@y. (x,y) : R)"

当我在谓词中编写以下内容时：

FORALL x. balance %^ x = Bbalance %^ x

其中 balance 和 Bbalance 都是偏函数（在 Z 中），在 Isabelle 中的形式为 ('a <=> 'b)，我认为它表现良好。

我如何定义另一个函数，我说这两个部分函数对于所有 'x' 都是完全不相交的。我的意思是相同值在两个偏函数“balance”和“Bbalance”上的关系应用永远不会产生相同的值。就像是...

FORALL x. balance %^ x \noteq Bbalance %^ x

抱歉解释不佳。我们通过专家建议学习:)。

4

1 回答 1

1

您的 rel_appl_def 规则使用了 epsilon 函数。根据斯坦福哲学百科全书 (SEP)(*) 在 1921 年 (1922) 的汉堡演讲中，希尔伯特首先提出了使用选择函数来处理算术形式系统中的排中原理的想法。

epsilon 函数的支配公理如下：

 (A x) --> (A (@ A))

在经典逻辑中，由于 ex falso quodlibet，如果 (A x) 失败，则 (@A) 可以采取任何解释。这意味着当您提供不在域 dom R 中的参数 x 时，您的 rel_appl_def 规则会给出任何值。

因此，您想用作相等的可能是两个部分函数上的以下布尔函数 (^)：

 f ^ g = (dom f = dom g) & (!x. x : dom f --> f %^ x = g %^ x)

当 SEP 写作时，我无法理解的第二个可能是当前更感兴趣的是在定理证明系统 HOL 和 Isabelle 中使用 epsilon-operator，其中 epsilon-terms 的表达能力产生了显着的实际优势。

我在实践中看到了对部分函数的更简单的处理，即使用选项类型。因此，偏函数 f 仅属于类型 A => B 选项。但是当您无法更改项目中的类型时，寻求符合您要求的相等性可能更明智，上述定义可能是一个候选者。

再见

(*)
The Epsilon Calculus, Jeremy Avigad 和 Richard Zach
于 2002 年 5 月 3 日星期五首次出版；实质性修订 2013 年 11 月 27 日星期三
http://plato.stanford.edu/entries/epsilon-calculus/

于 2015-01-29T23:14:25.870 回答