Why not take the bilimit of these types? A=[B→A]+A0, I’m guessing. The MirrorBot mirror diverges and that’s fine. If you use a constructivist approach where every B comes with the expression that defined it, you can define such strategies as “Cooperate iff PA proves that the opponent cooperates against me.”.
Why not take the bilimit of these types? A=[B→A]+A0, I’m guessing. The MirrorBot mirror diverges and that’s fine. If you use a constructivist approach where every B comes with the expression that defined it, you can define such strategies as “Cooperate iff PA proves that the opponent cooperates against me.”.