A Relational Theory of Monadic Rewriting Systems, Part I
2021
/icons/hr.icon
description
モナド書換え系とでも言う？MARSと呼んでいる．
操作が副作用を持つ: $ R : A → T A
モナド: $ \mathrm{monad}\: \mathbb{T} = (T, \eta, \mu)と，書換え $ \Gamma : Rel(X, Y ) \to Rel(T X, T Y )は，上の副作用の記法をもとにクライスリトリプル的な感じで定義される．
副作用のあるcall-by-valueのラムダ計算のエンコードができている．