lambda-mmm(実用版)

元々のLambda-mmmは実際に使われているmimiumでの中間表現と比べて以下のような差がある

型

τ ::= ∣ ∣ ∣ ∣ u ni t R I_{n} τ * τ τ \to τ n \in N

v ::= ∣ ∣ ∣ ∣ ∣ u ni t R v * v λ x . e d e l a y (e, e_{t im e}, v_{b o u n d}) f ee d x . e R \in R

e_{p} ::= ∣ e ::= ∣ ∣ ∣ .∣ ∣ ∣ ∣ u ni t R e_{p} e, e x λ x . e l e t x = e in e e e d e l a y (e, e_{t im e}, e_{b o u n d}) f ee d x . e R \in R [t u pl e] [v a r] [ab s] [l e t] [a pp] [d e l a y] [f ee d]

E ::= () ∣ E :: (x, v)

\frac{E ⊢ e _{b o u n d} ⇓ v _{b o u n d}}{E ⊢ d e l a y e e _{t im e} e _{b o u n d} ⇓ d e l a y e e _{t im e} v _{b o u n d}} E ^{n} ⊢ λ x . e ⇓ c l s ( λ x . e , E ^{n} ) \frac{E ^{n - 1} ⊢ e ⇓ v _{1} E ^{n} , x \mapsto v _{1} ⊢ e ⇓ v _{2}}{E ^{n} , x \mapsto v _{2} ⊢ f ee d x e ⇓ v _{1}} \frac{E ^{n} ⊢ e _{c} ⇓ n n > 0 E ^{n} ⊢ e _{t} ⇓ v}{E ^{n} ⊢ i f ( e _{c} ) e _{t} e l se e _{t} ⇓ v} \frac{E ^{n} ⊢ e _{c} ⇓ n n ≦ 0 E ^{n} ⊢ e _{e} ⇓ v}{E ^{n} ⊢ i f ( e _{c} ) e _{t} e l se e _{t} ⇓ v} \frac{E ^{n} ⊢ e _{1} ⇓ c l s ( λ x _{c} . e _{c} , E _{c}^{n} ) E ^{n} ⊢ e _{2} ⇓ v _{2} E _{c}^{n} , x _{c} \mapsto v _{2} ⊢ e _{c} ⇓ v}{E ^{n} ⊢ e _{1} e _{2} ⇓ v} [E-DELAY] [E-LAM] [E-FEED] [E-IFTRUE] [E-IFFALSE] [E-APP]