isabelle - 完全替换 isar 中的内部语法？

Question

我有兴趣使用 Isar 作为一种元语言来编写关于J的正式证明，这是一种可执行的数学符号和编程语言，我希望能够使用 J 作为内部语法。

J 由大量原语组成，并为每个 ASCII 字符分配（多个！）含义，包括单引号和双引号。

我在哪里可以找到实现全新内部语法的文档或示例代码？或者这甚至可能吗？（我一直在src/目录中四处寻找，但它有点压倒性，我不完全确定我在寻找什么。）

Answer 1

答案 B：以 HOL 为基础，使用即兴的 J 语法

澄清是好的，但我不喜欢进行必要的握手。

我在下面的第一个答案主要基于您的短语“一种全新的语法”，我认为这是对这样一个问题的答案的一半：

假设，假设我需要与 J 的语法非常接近的语法。关于 Isabelle/HOL，这需要什么？

我的答案：

1. 最有可能的是，我会说您必须取消定义 Isabelle/HOL 的常量、函数和类型类的大部分语法，这需要您对标准 Isabelle/HOL 发行版进行大量编辑才能将其取回在职的。Isabelle/HOL 中的一些语法，你很可能无法取出。
2. 或者，您必须重新开始，以导入Pure为起点。请在下面查看我的第一个答案。

只是语法？现在我们回到了正常的用户空间

Isabelle/HOL 中对语法的自定义使我们所有人都成为潜在的真正艺术家。

有一些高级方法可以利用定义语法的力量，例如parse_translation使用 Isabelle/ML，但我不使用高级方法。当我想重新排列函数的输入参数，或者不想弄乱标准 HOL 函数的符号时，我使用了一些基本关键字来定义语法：、、、notation和，no_notation以及。syntaxtranslationsabbreviation

notation, no_notation, 容易的

我用no_notation的不多，但你的武器库中需要它。例如，请参阅是否可以重载分配给 bool 和 list 的运算符的符号？.

notation一旦你看到几个例子，使用就很容易了。

对于中缀运算符 ,plus :: 'a => 'a => 'a以下是一些示例：

notation plus (infixl "[+]" 65)

notation (input) plus (infixl "[+]" 65)

notation (output) plus (infixl "[+]" 65)

通过这个例子，我进入了可能会弄乱 符号的领域plus，它是标准 HOL 类型类的运算符。

上面不会弄乱输出显示的行是使用(input).

对于notation，要查找示例，请在 THY 文件或文件夹中执行 greps src/HOL，因为有太多变体，无法在此处提供大量示例。

abbreviation，而不是把其他事情搞砸

假设我想要标准even谓词的非常紧密的绑定。我可以做这样的事情：

notation (input) even ("even _" [1000] 1000)
notation (output) even ("even _" [1000] 999)

我说“可以”，因为我不知道这会如何破坏 的标准函数应用even，所以我不想这样做。

为什么999？这只是来自反复试验和经验，我知道仅下一行就搞砸了declare[[show_brackets]]：

notation even ("even _" [1000] 1000)

这就是定义语法的方式。它是反复试验的结合，寻找用作模板的示例，经验，并在以后注意到你搞砸了一些事情。

abbreviation我忘记了所有帮助我的事情。的创新使用abbreviation可以使您不必使用更复杂的方法。

您可以使用它来重新排列参数，出于某种符号目的：

abbreviation list_foo :: "'a list => 'a => 'a list" where
  "list_foo xs x == x # xs"
notation 
  list_foo ("_ +#+ _" [65, 65] 64)

该示例是几个示例中的一个示例。我只是想举一个简单的例子，我有类似(infixl "_ +#+ _" [65, 65] 64). 我定义符号的方式没有太多变化，所以我必须找到一个例子Set.thy来告诉我我需要去掉infixl，因为我想[65, 65] 64用作如何定义语法的变体。

我是否得到了正确的优先级[65, 65] 64？我不知道。这只是一个简单的例子。

syntax和translations

你必须将它放在你的武器库中，但这会给你带来很多耗时的悲伤。执行 greps 并查找示例。试试这个那个。当你偶然发现一些有用的东西时，你认为你需要它，然后把它保存在某个地方。如果你不这样做，并且你做了一个小改动，破坏了你拥有的东西，并且你没有保存你曾经工作的东西，你会后悔不得不花费大量时间试图恢复工作。

Isar参考手册 isar-ref.pdf#175有一些信息。此外，您可以查看notation该 PDF 中的使用情况。

答案 B 部分未要求的部分

在您的评论中，您这样说：

我已经有了想要实现的“编程逻辑” （cs.utoronto.ca/~hehner/FMSD），J是一种特别适合正式证明的语言。我只是想弄清楚如何重用 Isabelle 的逻辑基础架构，而不是自己编写。

对于这样的问题，即使是对冲的问题，任何人都会给出一个简短的、不安全的答案，就像：

在 Isabelle/HOL 中，你很可能无法用 J 做你想做的事情。

一个更安全、更简短的答案是这样的：

最有可能的是，您在尝试使用 Isabelle/HOL 中的 J 做您想做的事情时会遇到重大问题。

这些都是简短而快速的答案。如果它实际上试图解决原因，那么对这样一个问题的回答怎么能简短呢？

它最终是一个“给定我所知道的一切”的答案，因为很多时候不是它不能完成，而是正确的一群人，给定足够长的时间，给定正确的技术，没有还没有做到。

我下面的标题成为我的观点。我试着很快地把剩下的东西吹透，但仍然记录下来。

通过您使用 HOL 作为您的逻辑，如果稍作修改，我的原始答案仍然适用

从Robin Milner开始，Isabelle/HOL 发展成今天的样子，我将其归类为火箭科学逻辑。

从我所有的搜索和我的所有聆听来看，似乎仍然需要开发大量火箭科学逻辑，然后才能使用证明助手正式验证以任何ole 命令式编程语言编写的任何 ole 程序。

你有一个逻辑，HOL，但你暗示你要实现的东西类似于很多人想要的东西，并且已经想要了很长时间。

下面的内容是为了支持我在这里所说的。

J 作为一种非常适合形式证明的语言

会有传统形式的算法分析，例如Cormen & Leiserson的《算法导论》第 3 版。

我将在 Isabelle/HOL机械化证明和形式验证程序中称为程序证明。我还认为某些纸笔校样是正式的。

那么，在传统的、非机械化的证明中，是的，我猜 J 是一种非常适合形式证明的语言，我这么说是因为你告诉我它是。但是，大型、流行的编程语言，特别是 C++ 和 Java，有关于形式化算法分析主题的教科书。因此，必须通过传统的、非机械化的证明，也可以对其进行推理。

J 在机械化证明的背景下

不，它不是一种非常适合正式、机械化证明的语言。它使用（比使用更好的词？）命令式编程，而且它似乎是面向对象的。

很大程度上，我只是在重复我读过别人说的话。我将开始发表声明作为我的个人结论。这会让事情变得更短。

函数式编程语言适用于形式证明。传统编程涉及变异变量，据说这会提高证明的难度。

我在邮件列表中搜索关于面向对象语言的声明，但如果你听，人们会说他们已经完成了这个或那个特别的事情，但它从来没有像，“这是一个完整的开发和形式化，很容易让你验证用通用编程语言 X 编写的程序”。

形式证明，除其他外，是关于一组公理的强制执行，其中公理的选择是火箭科学逻辑多年来的结果，因为规范并不要求一组看似合意的公理在逻辑上是合乎逻辑的持续的。

对于形式验证，您不能绕过公理的强制执行。在教科书中，数字常数只是出现并被使用，并且他们对它们进行推理。

在形式证明中，数字常数，尤其是实数，很难使用。问问自己，“什么是 Isabelle/HOL 中的自然数、整数、有理数和实数常数？” 现在，如果你回答了这个问题，那么问问自己，“我如何在 Isabelle/HOL 中进行涉及自然数、整数、有理数和实数的证明？”

现在，将这些问题与大多数教科书中出现的数字常数这一事实进行对比，并被使用。这不是它在正式证明中的工作方式。数字系统和常数没有神奇的外观。涉及数字的证明自动化可能有一点魔力，但我很确定如果我的计划依赖于这样的魔法，我注定要失败。

L4.verified（和自动更正）

有 NICTA 的L4.verified 项目。（更新：在sel4.systems中，与通用动力 C4 系统公司合作。像 GD 这样的大牌公司参与支持我的论点，即命令式编程语言的形式验证是长期以来非常需要的东西。 )

一个报价：

我们选择了一个操作系统内核来证明这一点：seL4。它是一个小型的第三代高性能微内核，大约有 8,700 行 C 代码。

为什么这么有选择性？为什么没有任何 ole C 程序？我想验证 C 很难。NICTA，他们不是一个小的、没有经验的、没有资金的团体。

（更新：在 NICTA 也有相关的AutoCorres 项目，及其快速入门指南 PDF。发布版本为 v1.0，于 2014-12-16 发布。这一定意味着他们实现了无论它是什么的主要目标他们应该实现。当我在 AutoCorres 网页上阅读他们的概述时，我认为它支持我所说的内容。在我看来，他们参与了一些火箭科学逻辑，至少将 C 转换为另一种形式一点火箭科学逻辑。我对什么构成火箭科学逻辑没有权威。我想我可以肯定地说他们正在使用博士级别的逻辑来获得他们的结果。）

编程实用理论一书：数字常量从何而来？

我下载了A Practical Theory of Programming一书的 PDF 。

我开始在那本书中寻找的第一件事是“什么是数字以及它们是如何形式化的”。

数字系统，我们认为它们是理所当然的，但它们代表了形式证明的所有困难。

在书中，当数字常量刚刚出现并开始被使用时，很可能意味着相应的数字系统没有真正的形式化。为什么？建立数字系统常数是非常复杂的。

如果没有正式建立数字常数，那么那里就没有真正的正式证明。如果他们真的建立起来，生活仍然不容易。

以下是与真正麻木一起工作的困难：Larry Paulson 2014 年在 NASA 的演讲。

编程实用理论一书：while循环

我立即开始寻找的另一件事是传统循环的示例，您可以在其中反复修改变量。

它从第 5.2.0 节 While 循环 aPToP.pdf#76开始。示例在下一页，练习 265：

while ¬ x = y = 0 do
    if y > 0 then y := y - 1
    else (x := x - 1. var· y := n)

你去吧，一个使用可变状态的经典示例（我在“可变状态”上进行了搜索以实际查看我是否正确使用了该短语，但没有明确的结论）。

你有一个变量，你正在改变它的内容。我听说，或者我得出的结论是，这代表了当你想要验证你用 J 编写的程序时，你注定要失败的原因。

并不是我要你注定失败。当您在 GitHub 上发布“Isabelle/HOL 中 J 编程语言的形式化 - 许多演示表明 J 程序可以轻松地被形式化验证”时，我会在那里。

考克。命令式编程有什么？

我有这样的预感，如果我的主要应用程序是编程，Coq 会更好。

我通过在coq 命令上进行谷歌搜索来保持最低要求。

第一个链接是Ynot。

这是否支持您的想法，即您应该能够采用 J 并在 Isabelle/HOL 中实施它？

不是我。它支持我的想法，即如果某人知道很多，并且能够就他们将要使用的语言做出设计决定，那么他们可以在证明助手中对命令式程序进行形式验证。

另一方面，您首先选择编程语言，然后围绕它塑造一个证明助手。

我对 J 的兴趣，从 0 到 10

在这一点上，我对 J 的兴趣基本上是 0，从 0 到 10。

但是，假设您建立了一个网站，“J Thing 的情况如何”，而我使用 RSS 阅读器订阅它。

不是我不想让你正式验证 Isabelle/HOL 中的 J 程序，而是我认为你做不到，所以我没有理由关心它，因为我不不需要它。

但是，如果我在我的 RSS 阅读器中为您的网站看到新活动，并且它告诉我您成功了，并且您将代码放在 GitHub 上，那么我的兴趣就转到了 10。有人在 Isabelle 为成熟的编程语言进行形式化/HOL，可以很好地实现证明，比如函数式编程，而不仅仅是语言的一小部分，这是值得感兴趣的。

原始答案

四天过去了，放假了，专家可能不会出现，所以我给你我的答案。

我试图尽快得到简短的答案，但我先说几件事（实际上，很多事情），试图给我的快速回答一些支持。

我不认为您使用 Isabelle 的词汇很正确（“内在语法”），但我采用了您的两个短语，并加了粗体强调：

1. 我有兴趣使用 Isar 作为一种元语言来编写关于 J的正式证明......
2. 我在哪里可以找到实现全新内部语法的文档或示例代码？

我不想花时间澄清，所以这就是我的要求说过：

1. 您需要一个可用于推理您用 J 编写的程序的逻辑，其中您使用 Isabelle/Pure 的最小逻辑作为起点（因为您需要 J 的完整语法，并且想要重新开始）。
2. 您想使用 Isabelle/Isar 定义语法，它实现（或模型？）J 的完整语法和功能。（您没有说您只想推理 J 的语法和功能的子集。）

不幸的是，我的简短回答还没有完全成立。

为了让您了解您的要求，我现在引用 J 主网页，重点是我的：

J 是一种现代的、高级的、通用的、高性能的编程语言。

我现在将通用重新表述为成熟的，就像 C、Pascal 和许多高级的通用编程语言一样，我提醒你，你想要两件事：

1. Isabelle 中的逻辑，在复杂性、功能和力量上肯定必须与 Isabelle/HOL 的逻辑相媲美。
2. Isabelle 中成熟的编程语言 J 的语法和使用（或建模？），从 Isabelle/Pure 开始，您的实现肯定必须在其中
   • 与 Isabelle/HOL 的代码生成器在复杂性和功能上有点可比，它可以导出 5 种编程语言的代码，SML、OCaml、Haskell、Scala 和 Eval (Isabelle/ML)，
   • 并且在功能上与 Isabelle/HOL 的逻辑引擎相媲美，它实现（或模型？）高级函数式编程结构，例如definition、primrec、datatype和fun，它允许人们定义函数和新数据类型，以及标准库Isabelle/HOL 类型，例如对、列表等。

现在，我声称，作为我个人的结论，您想要实现的至少与 Isabelle/HOL 一样难以实现，这是很多人多年来完成的结果。

请考虑一下 Peter Lammich 在I need a fixed mutable array中的 Isabelle 用户列表中所说的话：

HOL 本身不支持可变数组。

但是，有 Imperative_HOL，它有一个支持可变数组的堆 monad。

然后是 afp/Collections/Lib/Diff_Array，它提供了一个数组的实现，其行为纯粹是功能性的，但如果只访问最后一个版本，则效率很高。

但是，如果您不追求高效的可执行性，而只是寻找内存的抽象模型，那么使用上述类型是没有意义的，因为效率是以额外的形式化开销为代价的。

我的观点是，Isabelle/HOL 虽然强大到足以成为证明助手的领先竞争对手之一，但并未在其逻辑的主要部分实现标准数组，这是您在 import 时得到的Complex_Main。

让我们(L, P)成为一对，L逻辑在哪里P，编程语言在哪里。我想谈谈两对，(Isabelle/HOL, Haskell)，以及你想要的，(x, J)，x你尚未确定的逻辑在哪里。

Isabelle/HOL 和 Haskell 之间有着非常密切的关系。例如，Isabelle/HOL 的类型类被宣传为类似于 Haskell 的类型类，而且 Haskell 是一种纯函数式编程语言，而 Isabelle/HOL 是纯的。我不想更进一步，因为作为一个非专家，我肯定会说一些不对的东西。

我想说的是：

1. Haskell 是一门成熟的编程语言，
2. Isabelle/HOL 是一个强大的逻辑，
3. Haskell 是可以从 Isabelle/HOL 导出的编程语言之一，
4. 但是 Isabelle/HOL 并没有实现（或建模？）很多 Haskell。

我不想以某种权威的身份说话。但从听来，我的结论是：这是逻辑上的事情。显然，实现编程语言比开发逻辑来推理程序要容易得多。

简短的回答是，在我看来，您正在寻找的示例代码是 Isabelle/HOL，因为尽管在Isabelle2014/src其他逻辑中有一些示例，但我引用了您所说的和想要的，以及我的我说你在说和想要，是你想要并且需要一个full blown逻辑，比如 Isabelle/HOL。

从这里，我尝试抛出一些快速的想法。

我喜欢那辆车，但我真正想要的是液氮作为燃料

那是我的笑话。

你在和一位在这个行业工作多年的高级工程师交谈，并且学习了多年来在汽车行业积累的专业知识，你说，“我喜欢那种关于汽车的想法，但我的想法是使用氮燃料电池而不是汽油。我该怎么做呢？

Isabelle2014/src 文件夹中的更多逻辑

分发网页上Isabelle2014 的 Theory 库下的链接与文件夹中的Isabelle2014/src文件夹匹配。

在src文件夹中，您将看到文件夹CCL、Cube、CTT和其他文件夹。

我相信这些对学习很有帮助，虽然可能仍然难以理解，但这些不是你所描述的。您要求对编程语言建模的东西进行完整的实现。

如果 C/C++ 的用途如此之大，那为什么 C/C++ 没有你想要的东西呢？

我想至少有某种 C 语言。我找到了 vcc.codeplex.com/。再说一次，我不是专家，所以我不想确切地说那里有什么，什么不是。

我的意思是，C 和 C++ 已经存在了很长时间，并且被大量使用，上面的链接表明，长期以来，有专业人员对验证 C 程序感兴趣，这很有意义.

但是，经过这么多年，为什么程序验证不是 C/C++ 编程的一个组成部分呢？

从这里和那里，在邮件列表上听过那些人，从听过像 Scala 架构师 Martin Odersky 这样的人，他们永远想谈论可变和不可变状态，传统编程，如 C，我假设 J ，将属于使用可变状态的类别，非常使用它。随着时间的推移，我多次听到可变状态使我们难以推理程序的功能。

我的观点是，设计编程语言一定比推理程序容易得多。

最后，一点来源

如果这个问题有一些竞争，我可能会不那么冗长，虽然可能不是，虽然可能是这样，因为甚至没有给出答案。

我的最后一点是再次强调上述几点。了解一点历史是值得的，我在 Church 和 Curry 之前就开始了。

我知道 Isabelle/HOL 是从剑桥开始的结果，与 ML 的作者 Robin Milner，然后是 HOL 小组的 Mike Gordon，然后是使用 Pure 作为最小逻辑来定义其他逻辑的作者 Larry Paulson，以及然后 Tobias Nipkow 与他合作，在 Isabelle 中将 HOL 作为逻辑开始，然后 Makarius Wenzel 将更高级别的语法放在这一切之上，Isar（它不仅仅是语法糖；它是结构化证明功能的基础），连同 PIDE 前端，以及世界各地的其他人都做出了许多贡献，其中许多来自德国 TUM 的大团队，但还有澳大利亚的 CERN（更新：欧洲核子研究中心？这不是开玩笑；我确实知道 CERN 和 NICTA 之间的区别。世界，这不是一件容易谈论的事情），然后回到欧洲地区，某个瑞士机构，ETH，以及遍布德国和奥地利的更多地方，UIBK，然后回到英国？我遗漏了谁？当然，我和世界各地的许多其他人。

散漫点？正是你要求的东西体现了一个行业的专业知识。要求它也不错。这是彻头彻尾的大胆，我所说的可能完全错误，并且错过了通用编程语言实现逻辑src的HOWTO 中的那个文件夹，所有这些都是十个最简单的步骤，现在寄出你的 9.95 美元，或者欧元如果这就是你所拥有的一切，你做转换，我相信你，但是等等，还有更多，做一个更改目录到 Isabelle2014/medicaldoctor 并学习如何成为一名脑外科医生，也是。

我声称这是另一个笑话。只是一个空间填充物，仅此而已。

无论如何，请考虑这里的第 47 到 60 行HOL.thy：

setup {* Axclass.class_axiomatization (@{binding type}, []) *}
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}

axiomatization where fun_arity: "OFCLASS('a ⇒ 'b, type_class)"
instance "fun" :: (type, type) type by (rule fun_arity)

axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
instance itself :: (type) type by (rule itself_arity)

typedecl bool

judgment
  Trueprop :: "bool => prop" ("(_)" 5)

定期地，我努力理解这几行。很长一段时间以来，我的出发点是，除了importtypedecl bool之外，我并不关心试图理解之前是什么。HOL.thyPure

最近，在尝试找出 Isabelle 中的类型和分类时，我听了专家的意见，终于看到这条线是我们得到类似的地方x::'a::type：

setup {* Object_Logic.add_base_sort @{sort type} *}

还有一点？我回到我之前说的。因为你想要全面，所以你的例子是 Isabelle/HOL，但只是前 57 行HOL.thy并不容易理解。但是如果你不从HOL开始，你要去哪里看？好吧，如果你发现事情最终很容易，那很有可能部分是因为数百人多年来没有把他们的努力放在开始事情的最佳方式上。

或者，它可能只是被列为作者的 3 个人，Nipkow、Wenzel 和 Paulson。无论如何，其中的内容仍然有多年的经验和教育，尽管HOL.thy没有那么长，只有 2019 年的线路。当然，要了解其中的内容HOL.thy，您至少必须对其中的内容有一个模糊的了解Pure。

看看src/Cube文件夹。这是我上面提到的示例逻辑之一。

只有两个文件，Cube.thy和Example.thy. 这应该很容易，但那就是问题所在，太容易了。它不会反映 Isabelle/HOL 的复杂性。

你的问题不是我的问题。Isabelle/HOL 非常适合数学推理，例如它能够使用类型类抽象运算符。它还有利于更多，例如使用函数式编程定义函数，以便为 OCaml、Haskell、SML、Haskell 和 Eval 导出。

我只是一个初学者，这就是我的全部。如果有更好的答案，那么我希望有人提出。

Answer 2

关于原始问题的几点说明：

• 外层句法是 Isar 的理论和证明语言；要更改它，您需要定义其他命令。您受制于一般类型的理论内容，例如theory、local_theory、Proof.context，但这些类型非常灵活，可以吸收特定于您的应用程序的任意 ML 数据。

• 内部语法是逻辑的类型/术语语言，即 Pure 用于框架，HOL 用于应用程序（或您喜欢的任何其他逻辑，尽管 HOL 今天如此先进，您不应在没有充分理由的情况下忽略它）。最终你拼出简单类型的 lambda 项。

对于外部和内部语法，您都受制于某些标记概念（标识符、带引号的字符串等）。如果要与现有语法框架直接共存，则您的语言需要符合这一点。

尽管如此，还是可以通过使用引号将完全不同的语言嵌入到 Isabelle 的外部和内部语法中。例如，查看基于 LaTeX 的文档准备语言，并由{* ... *}逐字文本的有趣标记分隔。更基本的引用使用" ... "类似于 ML 字符串语法。在内部语法中，'' ... ''（双单引号）做了类似的工作。

在 Isabelle2014 中，有一种新的文本旋转图形句法设备，使这项工作更加顺畅。例如，请参阅Isabelle2014/src/HOL/ex/Cartouche_Examples.thy其中探索一些可能性的示例。

Isabelle2014 的另一个当前示例是 Isabelle 文档源中的铁路语言：它几乎可以作为从头定义的“特定于域的形式语言”的独立示例。例如，查看并查看在有限大小文件中Isabelle2014/src/Doc/Isar_Ref/Document_Preparation.thy的各种用途，需要仔细研究以了解更多信息。@{rail ...}Isabelle2014/src/Pure/Tools/rail.ML