ATS и арифметика в типах

[thedeemon]

Сегодня тема попроще

Comments

[diam_2003]

А ещё кроме "работы с матрицами" в боевой практике встречается богомерзская косвенная адресация...

Я это к тому, что у этой машинерии есть много применений в реализации вычислительных и "не очень" алгоритмов в различных параллельных средах, и там практические примеры, где всё совсем не радужно, сыпятся, как из рога изобилия.

Это, конечно, не умаляет достоинств ATS как языка, демонстрирующего мосчь "доказательного программирования" на примерах, доступных для современного уровня развития технологии.

[anonymous]

Неразрешимость случая когда есть умножение следует, в том числе, из неразрешимости диофантовых уравнений.

[si14]

Интересно, правильно ли я понимаю, что какая-нибудь Agda, в отличие от ATS, умеет ограничено выводить доказательства сама даже в случаях с умножениями?

[thedeemon]

В тред призывается nivanych! :)

[nivanych]

Вроде, permea_kra поболее возился с агдой и его призывать более уместно.

[diam_2003]

Agda может всё, для чего можно выписать алгоритм доказательства. В этом смысле она мощнее ATS. Есть ли там в библиотеках что-то кроме классики (Пресбургер, "хорошие" временные логики, политопы, ...) - не знаю.

[madf]

"... позволяют связать логически связать..." - одно "связать" лишнее.
Спасибо за интересный цикл!

[thedeemon]

поправил, спасибо!