时间戳

首页 > 解决方案 > 如何派生语言的语法（来自《类型和编程语言》一书）？

types - 如何派生语言的语法（来自《类型和编程语言》一书）？

问题描述

我正在阅读Types and Programming LanguagesBenjamin C. Pierce 的书。作者在第 3 节中谈到了一种语言的派生语法。第 3.2.3 节有以下内容。

对于每个自然数 i，定义一个集合 S1 如下

S0 = Empty Set
S(i+1) = {true, false, 0} Union {succ t1, pred t1, iszero t1 | t1 in Si}
         Union {if t1 then t2 else t3 | t1, t2, t3 in Si}
Finally, let
S = Union of Si (starting with i = 0)

然后作者说，由此我们可以得出那S0是空的。S1只包含常量。S2包含常量加上可以用常量和只有一个 succ、pred、iszero 或 if 构建的短语。这意味着什么？你是怎么推导出来的S2

标签： typessyntaxinduction

解决方案

(1) S_0 = ∅

(2) S_{i+1} = {true, false, 0} 
              ∪ {succ t1, pred t1, iszero t1 | t1 in Si}
              ∪ {if t1 then t2 else t3 | t1, t2, t3 in S_i}

(3) S = ⋃ {S_i} (starting with i = 0)$

这是一种使用集合构建器符号以归纳方式描述语言的方式。每个较大的索引S将包含较小索引术语的子S术语。让我们解决它给你一个想法。

我们知道这S_0是一个空集，因此它不包含任何术语。S_1是一组常数。

S_1 = {true, false, 0}

通过将 i = 1 放入等式（2）中，我们可以生成S_2

S_2 = {true, false, 0} 
    ∪ {succ t1, pred t1, iszero t1 | t1 in S_1}
    ∪ {if t1 then t2 else t3 | t1, t2, t3 in S_1}

S_2包含术语的集合也是如此：

S_2 = { true, false, 0, 
        succ true, pred true, iszero true, succ false, pred false, 
        iszero false,  succ zero, pred zero, iszero zero, 
        if true then true else true, if true then true else t3 false, 
        if true then true else t3 zero, if true then false else t3 true, 
        ..., if false then zero else zero, if zero then zero else zero}

请注意，S_2 中的项的子项只能是 S_1 中的项，即常数。因此，succ、pred、iszero 和 if 只会出现一次。

S_3将包含这样的条款，其中条款S_2和S_1是其子条款。所以它可以有 1 或 2 次出现 succ、pred、iszero 和 if。

本质上，您可以将其视为模板中t1的一个孔，您可以在其中插入术语。最后，完整的语言是所有这些 S_i 术语的联合。S_{i+1}S_{i}S

推荐阅读