Alloyで直積を考える （direct product in Alloy）

direct_product.als

/**
  Alloyで直積を考える
  cf. http://d.hatena.ne.jp/bonotake/20140414/1397488714
      http://d.hatena.ne.jp/m-hiyama/20140417/1397718771
*/
sig A, B, C {} -- univを豊かにするために置いておく

one sig Unit {}

check {
  all a: set univ {
    #(Unit -> a) = #a
    #(a -> Unit) = #a
  }
}

fun diagP (a: univ): univ -> univ {
  a -> a
}

fun joinL (a: univ->univ, r: (univ->Unit)->(univ->Unit)): Unit->Unit {
  (a.univ).(r.univ.univ) -> (univ.a).(univ.(univ.r))
}

fun ro (r: Unit -> Unit): Unit {
  Unit.r
}

fun prodL (f,g: univ -> Unit): univ -> Unit {
  {x: univ, u: Unit | u = x.diagP.joinL [f -> g].ro }
}

equiv_product: check {
  all f, g: univ -> Unit | prodL[f, g] = f & g
}