search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

L_to_Hyb: shifting problems #47

Closed Ayertienna closed 11 years ago

Ayertienna commented 11 years ago

We have 3 options for fetch:

M -> N ---> fetch w M -> box (unbox w+ N) M -> shift N ---> fetch w M -> box (unbox w+ (shift N)) M -> N ---> fetch w M -> box (unbox w+ (shift N))

Problem: first two options give us typing preservation. The last one gives preservation of world opening (which we need if there is ever going to be any dynamics).

Also, last one will allow us to use function instead of relation :)

Ayertienna commented 11 years ago

Bottom line is: without some idea of when shifted terms have types, we cannot use the last (nicest) solution.

Ayertienna commented 11 years ago

Done with a different (magic!) rewrite