首页 文章

如何定义合金中的双射(一对一)关系

提问于
浏览
0

我有三个合金签名如下:

sig A{}
sig B{}
sig C{}

如何定义C和A B之间的双射关系(或同构) .

1 回答

  • 0

    双射关系需要是内射和满射的 . 所以答案如下:

    sig A {}
    sig B{}
    sig C{r : one A+B}
    
    fact { 
        all c1,c2: C | c1.r=c2.r implies c1=c2   // r is injective
        all ab: A+B | some c:C | c.r=ab   // r in surjective
    }
    

    可能有更短的方式来写这个 . 其他人可能会发表评论 .

    谢谢

相关问题