Release 1.0.0

この項目はしばらくはずっと未完成です。。。

操作的意味論

//構文------------------------

//式
e :=
     t
     e op e

//演算子
op := +
      -
      /
      *
//項
t  := 
     n //数値
     x //変数
　　 λx.e //ラムダ抽象
     t t //関数適応
     (e)　//丸括弧で包まれた式
     {e1,...en} (n∈N n>0 正し、n=1の時は{e1}とする ) //tuple 
     {} // unit tuple

//値
v  := n
      x
      λx.e
      {v1,...vn} (n∈N n>0)
      ()

//文脈
ctx :=　φ　//空文脈
        ctx ∪ x:T //変数の束縛

//評価---------------------------

//演算子適応
e1 op e2 => e1  op e2' (e2=>e2')
e1 op v2  => e1' op v2   (e1=>e1')
v1  op v2  => v3

//関数適応
t1 t2 => t1' t2 (t1 => t1')
(λx.t12) t2 =>[x->t2]t12

//括弧
(e1)=>(e1') (e1=>e1')
(v1) =>v1

//tuple
{e1,...en} => {e1',...en} (e1=>e1' n∈N n>0 ) 
{v1,...vm,em+1,...en} => {v1,...vm,em+1',...en} (em+1=>em+1' n,m∈N n>m>0)

//型
T  := Int32
      {T1,...Tn} (n∈N n>0 )
      {}
      T->T

//型つけ---------------------------

//変数
 x:T (x:T ∈ ctx)

//関数適応
t1 t2 :T12 (t1:T11->T12 かつ t2:T11)

//数値
n:i32

//演算子
e1 op e2 :Int32 (e1:i32 , e2:i32)

//括弧
(e1) :T (e1 :T)