В Haskell есть функция (.) :: (b -> c) ->

Question

В Haskell есть функция (.) :: (b -> c) ->

(a -> b) -> a -> c. Есть такая вещь, как Curry-Howard correspondence, благодаря которой высказывания можно сопоставить типам, а импликацию следующему типу a -> b.

И импликация вида a => b читается так: если a, то b.

Можно ли таким образом "прочитать" функцию композиции?

Я понимаю, как можно было бы прочитать следующее f :: ((a -> b), (b -> c)) -> a -> c (если из a следует b и из b следует c, то из a следует c)

#haskell #programming #russian

0

06.02.2022

11 ответов

22 просмотра

ㅤ Атеист Автор вопроса

Cheese Syrowiecki
так это же транзитивность импликации. если у нас е...

https://plfa.github.io/Connectives/ Вот здесь написано, что (a * b) -> c изоморфна a -> (b -> c) в силу закона (p ^ n) ^ m ≡ p ^ (n * m) (осталось лишь понять, почему этот закон работает, и как мы от закона переходим к изоморфизму)

0

07.02.2022

Cheese Syrowiecki

нельзя сказать «в силу», потому что вы фактически одну формулу записали на разных языках. получилось «доброе утро в силу good morning»

0

07.02.2022

ㅤ Атеист Автор вопроса

Cheese Syrowiecki
нельзя сказать «в силу», потому что вы фактически ...

А, ну я просто пересказал, что написано в книге: > Corresponding to the law > (p * n) ^ m = (p ^ m) * (n ^ m) > we have the isomorphism: > A → B × C ≃ (A → B) × (A → C) Может, я неправильно пересказал

0

07.02.2022

Cheese Syrowiecki

ㅤ Атеист
А, ну я просто пересказал, что написано в книге: >...

да, это соответствие Карри—Говарда, но это не доказательство

0

07.02.2022

Cheese Syrowiecki

ㅤ Атеист
https://plfa.github.io/Connectives/ Вот здесь нап...

уточните, от чего к чему переход интересует

0

07.02.2022

ㅤ Атеист Автор вопроса

Cheese Syrowiecki
уточните, от чего к чему переход интересует

Почему справедливо ((a * b) → c) \iff (a →(b →c)) в логике?

0

07.02.2022

ㅤ Атеист Автор вопроса

ㅤ Атеист
Почему справедливо ((a * b) → c) \iff (a →(b →c)) ...

Наверное, через законы какие-то можно вывести. (~(a * b) + c) \iff (~a + (~b + c)) (~a + ~b + c) \iff (~a + ~b + c) ((a -> b) \iff (~a + b)) (~(a * b) \iff (~a + ~b))

0

07.02.2022

Nutritional Rabbit

ㅤ Атеист
А, ну я просто пересказал, что написано в книге: >...