Symmetric Interaction Calculus in HVM2

sic.hvml

// COMPUTATION RULES
// ===================================================
// APP | ((λx body) arg)
//  X  | ---------------------------------------------
// LAM | x ~ arg; body
// ===================================================
// APP | ({fst snd} arg)
//  X  | ---------------------------------------------
// SUP | dup #L{a,b} = arg; {(fst a) (snd b)}
// ===================================================
// APP | ((dup #L{a,b} = val; bod) arg)
//  X  | ---------------------------------------------
// DUP | (dup #L{a,b} = val; (bod arg))
// ===================================================
// DUP | dup #R{a,b} = (λx f); bod
//  X  | ---------------------------------------------
// LAM | a ~ λx0 b0; b ~ λx1 b1; x ~ #L{x0,x1};
//     | dup #L{b0,b1} = f; cont
// ===================================================
// DUP | dup #R{a,b} = #R{r,s}; cont
//  X  | ---------------------------------------------
// SUP | a ~ r; b ~ s;
// ===================================================
// DUP | dup #L{a,b} = (dup #K{c,d} = val; bodK); bodL
//  X  | ---------------------------------------------
// DUP | dup #L{c,d} = val; dup #K{a,b} = bodK; bodL

// Type
// ----

data Term
  = (Lam bod)
  | (App fun arg)
  | (Sup fst snd)
  | (Dup val bod)
  | (Var exp) 

// Evaluation
// ----------

(Reduce x) = match x {
  Lam: (Lam x.bod)
  App: (Reduce.App (Reduce x.fun) x.arg)
  Sup: (Sup x.fst x.snd)
  Dup: (Reduce.Dup (Reduce x.val) x.bod)
  Var: (Var x.exp)
}

(Reduce.App fun arg) = match fun {
  Lam: (Reduce (fun.bod arg))
  App: (App (App fun.fun fun.arg) arg)
  Sup: (Reduce (Dup arg λaλb(Sup (App fun.fst a) (App fun.snd b))))
  Dup: (Reduce (Dup fun.val λaλb(App (fun.bod a b) arg)))
  Var: (App (Var fun.exp) arg)
}

(Reduce.Dup val bod) = match val {
  Lam: (Reduce (Dup (val.bod (Sup $x0 $x1)) λb0λb1(bod (Lam λ$x0(b0)) (Lam λ$x1(b1)))))
  App: (Dup (App val.fun val.arg) bod)
  Sup: (Reduce (bod val.fst val.snd))
  Dup: (Reduce (Dup val.val λcλd(Dup (val.bod c d) bod)))
  Var: (Dup (Var val.exp) bod)
}

// Normalization
// -------------

(Normal term) = (Normal.go (Reduce term))

(Normal.go term) = match term {
  Lam: (Lam λx (Normal (term.bod (Var x))))
  App: (App (Normal term.fun) (Normal term.arg))
  Dup: (Dup (Normal term.val) λaλb(Normal (term.bod (Var a) (Var b))))
  Sup: (Sup (Normal term.fst) (Normal term.snd))
  Var: term.exp
}

Main =
  let id  = (Lam λx (x))
  let tru = (Lam λt (Lam λf t))
  let fal = (Lam λt (Lam λf f))
  let not = (Lam λb (Lam λt (Lam λf (App (App b f) t))))
  let n2  = (Lam λf (Lam λx (Dup f λf0λf1(App f0 (App f1 x)))))
  let n3  = (Lam λf (Lam λx (Dup f λf0λf1(Dup f λf2λf3(App f1 (App f2 (App f3 x)))))))
  (Normal (App (App n3 not) fal))