如何理解 Isabelle 中的句法和翻译

Question

我正在尝试理解 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, 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

的参考资料

Answer 1

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

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

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

命令translations和print_translation分别在8.5.2和8.5.3小节中解释。因此，translations 可用于指定 AST 的重写规则，而 print_translations 允许任意操作用于打印的内部语法（记住粗略的“term->AST->pretty printed text “ 顺序）。在这种情况下，您可以直接检查调用 print_translation 的效果，如下所示

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

print_translation ‹…›

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

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

如何理解 Isabelle 中的句法和翻译

How to understand syntax and translation in Isabelle

syntax

verification

formal-verification

formal-methods

isabelle