logic - 类型系统中实践规则归纳的任何文件？

Question

如您所知，要定义一个新的类型系统，一种方法是我们需要：

1. 语言语法
2. 打字规则

然后我们需要证明一些我们认为可以使用上述类型规则证明的定理。为了证明这些定理，一种方法是我们可以使用归纳法（Rule Induction）。

例如，我们有一个这样的系统：

nat n ::= 0 | S n

我们定义了 2 个规则“Zero”和“Succ”，如下所示：

                n nat 
_____ Zero     _______ Succ  
0 nat          S n nat 

然后，我们提出一个定理，我们认为这个定理是正确的，我们需要证明它。

If n nat, then S S n nat.

我们可以使用定义的规则轻松证明这个定理。这就是所谓的规则归纳。

那么有没有人知道可以帮助练习规则归纳的资源？

Answer 1

您可以通过使用结构归纳来证明这一点，但考虑到您不必在归纳步骤中使用归纳假设，这将是完全没有必要的。

为了向n nat -> S S n nat您展示简单的假设n nat和展示S S n nat，可以按如下方式完成：

 _____ (By assumption)
 n nat
 _______ Succ
 S n nat
_________ Succ
S S n nat