首页 文章

Haskell中有趣的操作符遵守模态公理

提问于
浏览 次
8

我只是看着 map :: (a -> b) -> [a] -> [b] 的类型，只是这个函数的形状让我想知道我们是否可以看到列表形成operator []遵循正常模态逻辑常见的各种公理（例如，T，S4，S5，B），因为我们似乎至少有正常模态逻辑的K-公理， [(a -> b)] -> [a] -> [b] .

这导致了我的问题：在Haskell中是否有熟悉的，有趣的运算符或函子，它们具有某种模态运算符的语法，并且遵循普通模态逻辑（即K，T，S4，S5和B）常见的公理 . ）？

这个问题可以更加清晰，更具体 . 考虑一个运算符 L ，它的双 M . 现在问题变成：Haskell中是否有任何熟悉的，有趣的运算符，具有以下某些属性：

（1） L(a -> b) -> La -> Lb

（2） La -> a

（3） Ma -> L(M a)

（4） La -> L(L a)

（5） a -> L(M a)

看到一些很好的例子会非常有趣 .

我想到了一个潜在的例子，但是知道我是否正确会很好：双重否定翻译 L 为 not not 和 M 为 not . 这个翻译将每个公式 a 都用于其双重否定翻译 (a -> ⊥) -> ⊥ ，并且，至关重要的是，验证公理（1） - （4），但不是公理（5） . 我在这里问了一个问题https://math.stackexchange.com/questions/2347437/continuations-in-mathematics-nice-examples似乎双重否定翻译可以通过延续monad来模拟，endofunctor将每个公式 a 带到它的双重否定翻译 (a -> ⊥) -> ⊥ . 德里克·埃尔金斯（Derek Elkins）指出存在一些双重否定翻译，通过库里 - 霍华德同构，对应于不同的连续传递风格变换，例如， Kolmogorov对应于按姓名调用的CPS变换 .

也许还有其他操作可以通过Haskell在continuation monad中完成，它可以验证公理（1） - （5） .

（并且只是为了消除一个例子：在Haskell中所谓的Lax逻辑https://www.sciencedirect.com/science/article/pii/S0890540197926274和Monads之间存在明确的关系，返回操作遵循该逻辑的模态运算符的规律（这是一个endofunctor） . 我不感兴趣所以在这些例子中，但在Haskell运算符的例子中，这些运算符遵循经典正态模态逻辑中的模态运算符的一些公理）

haskell logic

1 回答

  • 3

    初步说明：我很抱歉花了大量的答案谈论命题Lax逻辑，这是一个你对这个问题感兴趣的主题并没有太多兴趣 . 无论如何，我觉得这个主题值得更广泛的曝光 - 感谢让我意识到这一点！

    命题宽松逻辑（PLL）中的模态运算符是 Monad 类型构造函数的Curry-Howard对应物 . 注意它的公理之间的对应关系......

    DT: x -> D x
D4: D (D x) -> D x
DF: (x -> y) -> D x -> D y

    ......分别是 return ， join 和 fmap 的类型 .

    Valeria de Paiva有很多论文讨论直觉模态逻辑，特别是PLL . 关于PLL的评论主要基于Alechina et. al., Categorical and Kripke Semantics for Constructive S4 Modal Logic (2001) . 有趣的是，该论文使得PLL的情况不像最初看起来那么奇怪（参见Fairtlough and Mendler, Propositional Lax Logic (1997)："As a modal logic it is special because it features a single modal operator [...] that has a flavour both of possibility and necessity"） . 从CS4开始，直觉主义S4的一个版本没有分离的可能性......

    B stands for box, and D for diamond

BK: B (x -> y) -> (B x -> B y)
BT: B x -> x
B4: B x -> B (B x)

DK: B (x -> y) -> (D x -> D y)
DT: x -> D x
D4: B (B x) -> B x

    ...并向其添加 x -> B x 会导致 B 变得微不足道（或者，在Haskell的说法中， Identity ），简化了PLL的逻辑 . 既然如此，PLL可以被视为直觉主义S4变体的特例 . 此外，它将PLL的 D 帧化为类似可能性的运算符 . 如果我们把 D 作为Haskell Monad 的对应物，这是直觉上很有吸引力的，这通常有可能的味道（考虑 Maybe Integer - “这里可能有一个 Integer ” - 或 IO Integer - “我会得到 Integer 当程序执行“） .

    其他一些可能性：

    回复于

相关问题