@haskellru - страница 751 - Telegram web archive

Vladislav

что я могу взять и сколдовать тёрм x изниоткуда?

Евгений

https://en.wikipedia.org/wiki/Intuitionistic_logic

Евгений

См. PRED-1 и PRED-2

Vladislav

в статье не грепается даже "predicative"

Vladislav

ну круто, я вижу две аксиомы

Vladislav

которые добавляются ПОВЕРХ, чтобы то утверждение выполнялось

Евгений

Эм? Нет, это аксиомы интуиционистской логики предикатов первого порядка

Евгений

Конечно ты можешь вообще никаких аксиом на forall и exist не задавать. Но это получится другая логика

Vladislav

как квантифицирован t в тех аксиомах?

Vladislav

как мне читать это, forall x. f(x) -> forall t. f(t)? выглядит как альфа-эквивалентность

Евгений

, if the term t is free for substitution for the variable x in ϕ {\displaystyle \phi } \phi (i.e., if no occurrence of any variable in t becomes bound in ϕ ( t ) {\displaystyle \phi (t)} \phi (t))

Евгений

Никак, t ВНУТРИ языка логики не является переменной

Vladislav

если этот t из внешнего контекста, то выглядит как применение функции

Vladislav

ес-сно я могу взять и присвоить x = t если x универсально квантицифирована

Евгений

Блин, ты понимаешь, что это не теория типов? И речь идёт не о функциях, потому что нет никакой редукции, а о термах и выражениях?

Anonymous

t - терм, заменяющий все вхождения x в формуле фи

Anonymous

терм произвольный

Vladislav

> И речь идёт не о функциях Я так не умею, потому что читаю forall как функцию

Anonymous

тогда почитай что-нибудь по логике предикатов

Vladislav

И что мне потом делать с этим знанием? В любом proof assistant моделируется forall как функция

Vladislav

а exists как тьюпл

Евгений

Внезапно, но можно доказывать утверждения без пруф асистанта

Vladislav

всё что лишено операционной семантики меня как программиста не интересует

Евгений

Я даже скажу больше: любой пруф ассистент ограничен определённым рекурсивным ординалом

Vladislav

мне это ни о чем не говорит, к сожалению

Vladislav

речь изначально шла про forall в Haskell и его гипотетический counterpart exists (который мог бы быть добавлен в Haskell). forall представляет собой (в моем понимании) нерелевантную зависимую квантификацию

Евгений

При чём максимальный теоретически достижимый ординал сейчас соответствует \psi_{\Omega_1}\Omega_{{\rm M}+\omega}, это очень мало. Классическая математика оперирует намного большими универсумами

Vladislav

в этом ограниченном моем программистском мирке я не могу заключить exists из forall

Евгений

речь изначально шла про forall в Haskell и его гипотетический counterpart exists (который мог бы быть добавлен в Haskell). forall представляет собой (в моем понимании) нерелевантную зависимую квантификацию

Нет, это неправда. forall представляет собой System F квантификацию

A64m

Внезапно, но можно доказывать утверждения без пруф асистанта

мясные куклы могут что-то доказывать? звучит неправдоподобно

Евгений

С помощью пруф-асистента никто ничего не доказал вообще, это не более чем инструмент формализации

A64m

на каком-то программистском форуме вроде рсдн чуть ли ни при каждом упоминании пруф ассистанта какой-то математик примерно так отписывался

Евгений

Это был не я

Anonymous

лично я не вижу смысла работать с пруф-асистентами, не имея бекграунда в теории. а с бекграундом такие вопросы, как у тебя выше, отпадают сами собой

Anonymous

И что мне потом делать с этим знанием? В любом proof assistant моделируется forall как функция

Vladislav

> лично я не вижу смысла работать с пруф-асистентами, не имея бекграунда в теории Смысл в том, чтобы свойства моего кода доказывать

Vladislav

Который потом будет на компьютере выполняться, и в котором тёрмы не синтезируются словом "допустим существует x, который..."

Denis

С помощью пруф-асистента никто ничего не доказал вообще, это не более чем инструмент формализации

неправда, four-color theorem доказали

Зигохистоморфный

неправда, four-color theorem доказали

а где про проблему 4 красок?

Евгений

неправда, four-color theorem доказали

Эм? Нет. Там изначально было обычное доказательство, сводящее проблему к конечному числу случаев, а потом алгоритмический перебор. Потом в 2005'ом году всё свели вместе в рамках Coq

Vladislav

Хотя свою ошибку я тоже понял т.к. exists не пруфрелевантный, то синтезировать тёрм не придется

Vladislav

а потому exists x. P(x) можно сказать не предоставляя x

Vladislav

в отличие от сигма-типа

Евгений

O, ты почувствовал различие между System F и MLTT

Евгений

Чувствуется прогресс

Denis

Эм? Нет. Там изначально было обычное доказательство, сводящее проблему к конечному числу случаев, а потом алгоритмический перебор. Потом в 2005'ом году всё свели вместе в рамках Coq

я насколько знаю историю, то доказательство с помощью вычислительной части на ssreflect помогло как раз сомнения по поводу правильности доказательства устранить

Denis

т.к. смогли формализовать и проверить все ветки из пруфа

Vladislav

Чувствуется прогресс

Без прогресса спорить вообще было бы обидно и бесполезно. Хотя про разницу я и так знал, просто одна из этих систем для меня почти незнакома, а потому интуиция для нее не развита. Теперь осознал, что forall x. P(x) -> exists x. P(x) это корректное правило

Vladislav

в то время как Pi x P(x) -> Sigma x P(x) некорректное, и я это ошибочно обобщил

A64m

scala> collection.immutable.Seq(1,2,3) == collection.mutable.Seq(1,2,3) res0: Boolean = true СЕРЬЕЗНО? вычитал про это на хаскельреддите, даже полез проверять. А вы говорите жаваскрипт