Как вывести синтаксис языка (из книги «Типы и языки программирования»)?

Question

Я читаю книгу Types and Programming Languages Бенджамина С. Пирса. автор говорит о выводе синтаксиса для языка в разделе 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 или, если . Что это обозначает? Как вы выводите S2

Answer 1

(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+1}, в которую можно вставить S_{i} термины. Наконец, полный язык S является объединением всех таких терминов S_i.