如何理解伊莎贝尔的语法和翻译

编程问答 2022-04-22

问题描述

我正在尝试理解 Isabelle/HOL 中 Rely Guarantee 的代码，但对中的 Syntax 和 translation 关键字感到困惑 https://isabelle.in.tum.de/library/HOL/HOL-Hoare_Parallel/RG_Syntax.html

Syntax
  "_Assign"    :: "idt ⇒ 'b ⇒ 'a com"                     ("(´_ :=/ _)" [70,65] 61)
  "_Cond"      :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0,0] 61)
  "_Cond2"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
  "_While"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0WHILE _ /DO _ /OD)"  [0,0] 61)
  "_Await"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0AWAIT _ /THEN /_ /END)"  [0,0] 61)
  "_Atom"      :: "'a com ⇒ 'a com"                        ("(⟨_⟩)" 61)
  "_Wait"      :: "'a bexp ⇒ 'a com"                       ("(0WAIT _ END)" 61)
  "_PAR"       :: "prgs ⇒ 'a"                              ("COBEGIN//_//COEND" 60)

我对三个问题感到困惑

(1) 为什么名称前总是有一个下划线 _Assign？

(2)(´_ :=/ _)中的斜线和单引号和COBEGIN//_//COEND中的双斜线是什么意思

(3) 为什么在mixfix符号0IF _ THEN _ FI之前有一个零

translations
  "´x := a" ⇀ "CONST Basic «´(_update_name x (λ_. a))»"
  "IF b THEN c1 ELSE c2 FI" ⇀ "CONST Cond ⦃b⦄ c1 c2"
  "IF b THEN c FI" ⇌ "IF b THEN c ELSE SKIP FI"
  "WHILE b DO c OD" ⇀ "CONST While ⦃b⦄ c"
  "AWAIT b THEN c END" ⇌ "CONST Await ⦃b⦄ c"
  "⟨c⟩" ⇌ "AWAIT CONST True THEN c END"
  "WAIT b END" ⇌ "AWAIT b THEN SKIP END"

print_translation ‹
  let
    fun quote_tr' f (t :: ts) =
          Term.list_comb (f $ Syntax_Trans.quote_tr' \<^Syntax_const>‹_antiquote› t,ts)
      | quote_tr' _ _ = raise Match;

    val assert_tr' = quote_tr' (Syntax.const \<^Syntax_const>‹_Assert›);

    fun bexp_tr' name ((Const (\<^const_Syntax>‹Collect›,_) $ t) :: ts) =
          quote_tr' (Syntax.const name) (t :: ts)
      | bexp_tr' _ _ = raise Match;

    fun assign_tr' (Abs (x,_,f $ k $ Bound 0) :: ts) =
          quote_tr' (Syntax.const \<^Syntax_const>‹_Assign› $ Syntax_Trans.update_name_tr' f)
            (Abs (x,dummyT,Syntax_Trans.const_abs_tr' k) :: ts)
      | assign_tr' _ = raise Match;
  in
   [(\<^const_Syntax>‹Collect›,K assert_tr'),(\<^const_Syntax>‹Basic›,K assign_tr'),(\<^const_Syntax>‹Cond›,K (bexp_tr' \<^Syntax_const>‹_Cond›)),(\<^const_Syntax>‹While›,K (bexp_tr' \<^Syntax_const>‹_While›))]
  end
›

我无法理解上面代码的含义。我在哪里可以找到有关使用 translations 和 print_translation

的参考资料

解决方法

您要查找的信息可以在 Isabelle 的标准参考手册（Isar-ref 或 The Isabelle/Isar Reference Manual by Makarius Wenzel）的第 8 章中找到。更具体地说，请参阅参考手册中的第 8.2、8.4 和 8.5 小节。

就我个人而言，我不熟悉 Isabelle 中语法转换的实现细节，因此我的回答将依赖于文档中已经说明的内容。因此，我的建议是使用参考手册作为信息的主要来源。如果在学习了参考手册后，您还有其他问题，您不妨试试 Isabelle 或 Zulip chat 的邮件列表。

  1. 命令 syntax 在参考手册的 8.5.2 小节中进行了解释。在您的问题中，_Assign 是语法声明的语法常量，它只是 Isar 语言语法实体中的一个名称（参见参考手册中的第 3.2 小节）。从技术上讲，下划线应该没有特殊含义，但是在语法常量的名称开头使用下划线是一种约定，似乎只有语法常量的名称才能以下划线开头。
  2. 参考手册中的第 8.2 小节已经包含对您的第二个问题的相当详细的回答。 mixfix 模板 ´ 中的单引号 (´_ :=/ _) 没有任何特殊含义。但是，/ 允许（但不强制）换行，而 // 在漂亮打印期间强制换行。
  3. 一般来说，(n 和 n 是一个自然数，在 mixfix 注释中打开一个漂亮的打印块。数字 n 指定块缩进（即块中发生换行时添加的空格数）。但是，如果未指定 n，则应默认为 0。因此，我不完全确定为什么在这种情况下确实需要 0。您可能希望进一步调查。

命令 translations 和 print_translation 分别在 8.5.2 和 8.5.3 小节中进行了解释。因此，translations 可用于 AST 上重写规则的规范，而 print_translations 允许对用于打印的内部语法进行任意操作（请记住粗略的“术语->AST->漂亮的打印文本“ 顺序）。在这种情况下，您可以直接检查调用 print_translation 的效果，如下所示

lemma "´a := b = c"
  (*Basic (a_update (λ_. b)) = c*)
  oops

print_translation ‹…›

lemma "´a := b = c"
  (*´a := b = c*)
  oops

希望这会有所帮助，或者至少为您指明相关资源的方向。

formal-methodsformal-verificationisabelleverificationverification