petit

勉強を兼ねてpetitの実装

petitの構文領域

ζ:Var 識別子の全体
ε:Exp 式の全体
τ:Pro プログラムの全体

構文規則

(1) ζ ::= A | B | … | Z
(2) ε ::= 0 | ζ | suc ε
(3) τ ::= ζ := ε | τ;τ | for ε times do τ end

petitの意味領域

N 自然数の全体(0を含む)
S = (Var → N) コンピュータの状態全体
C = (S → S) コンピュータの状態の変換全体

意味関数

Ε : Exp → (S → N)
C : Pro → C

(1) E[[0]](σ) = 0
(2) E[[ξ]](σ) = σ(ξ)
(3) E[[suc ε]](σ) = E[[ε]](σ) + 1
(4) C[[ξ:= ε]](σ) = update(ξ, E[[ε]](σ))(σ)
(5) C[[τ1; τ2]](σ) = C[[τ2]](C[[τ1]](σ))
(6) C[[for ε times do τ end]](σ) = iterate(C[[τ]], E[[ε]](σ))(σ)

補助関数

update : Var * N → C
update(ξ, ν)(σ) = σ{ξ:ν}

iterate : C * N → C
iterate(θ, ν) = θ◦θ◦…◦θ