Я просто смотрел на тип map :: (a -> b) -> [a] -> [b], и сама форма этой функции заставила меня задуматься, можем ли мы видеть, что оператор формирования списка [] подчиняется различным аксиомам, общим для нормальной модальной логики (например, 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-matMathematics-nice-examples, и кажется, что перевод двойного отрицания можно смоделировать с помощью монады продолжения, эндофунктор переводит каждую формулу a в ее перевод двойного отрицания (a -> ⊥) -> ⊥. Там Дерек Элкинс отмечает существование пары переводов двойного отрицания, соответствующих через изоморфизм Карри-Ховарда различным преобразованиям стиля передачи продолжения, например Колмогорова соответствует преобразованию CPS по имени.
Возможно, есть другие операции, которые могут быть выполнены в монаде продолжения через Haskell, что может подтвердить аксиомы (1) - (5).
(И чтобы исключить один пример: между так называемой логикой Слабости https://www.sciencedirect.com/science/article/pii/S0890540197926274 и Monads в Haskell, при этом операция возврата подчиняется законам модального оператора этой логики (который является эндофунктором). Меня это не интересует. много в этих примерах, но в примерах операторов Haskell, которые подчиняются некоторым аксиомам модальных операторов в классической нормальной модальной логике)
as вbs. - person Willem Van Onsem schedule 13.03.2018[a -> b] -> [a] -> [b]- это тип(<*>), специализированный для[]экземпляраApplicative. - person Rein Henrichs schedule 13.03.2018(<*>) :: [a -> b] -> [a] -> [b], а также для модальности функции у нас есть(<*>) :: (e -> (a -> b)) -> (e -> a) -> (e -> b), который является хорошо известным комбинатором K. Вероятно, это просто совпадение, что они разделяют имя К. ;-) - person Daniel Wagner schedule 13.03.2018<*>какой-либо другой аксиоме нормальной модальной логики? - person user65526 schedule 13.03.2018Lконечно же выглядит как комонада, но не уверен, что этоMбыло бы навскидку. Но, например, известные комонады, такие как непустые спискиa, пары(w,a)подойдут. - person luqui schedule 14.03.2018extractпохож на (2) выше (аксиома T в модальной логике),duplicateпохож на (4) (аксиома S4). Простой пример оператора для (3) потребуетMдля обозначенияFalseиLдля обозначенияTruth, и эта интерпретация (очевидно) работает для некоторых других примеров. - person user65526 schedule 14.03.2018a, пары(w,a), чего бы удовлетворили, извините? - person user65526 schedule 14.03.2018ComonadApplyдля некоторых модальная логика. - person dfeuer schedule 14.03.2018Lкакnot notиMкакnotподтверждает все вышеприведенные аксиомы. Я задал этот вопрос здесь, math.stackexchange.com/ questions / 2347437 /, в которых я утверждал, что перевод двойного отрицания был примером монады продолжения. Эндофунктор в этом случае будет переводить каждую формулуaв свой перевод двойного отрицания(a -> ⊥) -> ⊥. - person user65526 schedule 14.03.2018a -> not (not (not a)), что кажется неприятным прикосновением. - person pigworker schedule 14.03.2018M≈MonadиL≈ComonadApply(# 1:(Applicative f) => f (a -> b) -> f a -> f b; # 2:extract :: (Comonad f) => f a -> a; # 4:duplicate :: (Comonad f) => f a -> f (f a)) или, возможно,MonadTrans(# 3:lift :: (MonadTrans t, Monad m) => m a -> t (m a); # 5:instance (MonadTrans t, Monad m) => Monad (t m) where return :: a -> t (m a)). Но я действительно работал только с эпистемической модальной логикой (□ = «заведомо истинно», ◇ = «заведомо не ложно»), не слишком знаком с модальной логикой в целом. - person Jon Purdy schedule 15.03.2018(Applicative f) => f (a -> b) -> f a -> f b, когдаf- комонада? Если это так, то оператор Comonadic синтаксически ведет себя как оператор необходимости модальной логики S4 (модальная логика, взаимно переводимая с интуиционистской логикой через знаменитый перевод Гёделя). Подчиняются ли монадные преобразователи какой-либо из других аксиом, перечисленных в моем вопросе? - person user65526 schedule 15.03.2018<*>- это комбинатор S, а не K. - person Will Ness schedule 03.10.2018