Разбираемся в рекурсии

    Привет, Хабр.



    Про рекурсию ходит много шуток, и она традиционно считается одной из сложных для понимания тем в computer science, поэтому давайте сегодня немного о ней поговорим. А именно, давайте обсудим, как выражать доказуемо завершимые вычисления.


    Зачем это надо? Рекурсия — один из краеугольных камней ФП, а некоторые из функциональных языков (например, Idris или Agda) обладают достаточно мощной системой типов, чтобы использовать их для проверки доказательств. А чтобы проверенным доказательствам на самом деле можно было доверять, было бы неплохо, чтобы логическая система, которую представляет система типов языка, была консистентна — то есть, если упрощать, чтобы в ней нельзя было доказать ложь.


    Один из главных источников неконсистентности — незавершающиеся вычисления (для примера см. КДПВ), поэтому вышеупомянутые языки очень стараются дать возможность убедиться, что вычисления завершаются — соответствующая их часть даже имеет отдельное название, «termination checker». Но, увы, по фундаментальным причинам у любой такой проверки всегда будут ложноположительные или ложноотрицательные срабатывания, поэтому приходится идти на компромиссы. В доказательствах лучше перебдеть, чем недобдеть, поэтому всегда есть завершимые функции, которые этими языками отвергаются. Однако, эти функции можно переписать так, чтобы termination checker был доволен, если можно доказать, что рекурсивный вызов всегда в каком-то смысле «меньше».


    Не так давно мне нужно было убедить Агду, что куча взаимно рекурсивных функций всегда завершается. Для этого пришлось почитать стандартную библиотеку и пораскрывать встречающиеся абстракции, чтобы понять, что же там на самом деле происходит. В процессе я делал заметки, а потом понял, что если добавить в эти заметки слова, то может получиться полезный кому-то ещё текст.


    Немного вводных


    Сначала определим одно слово, которое дальше будет часто встречаться. Фундированное отношение на множестве — это такое отношение, у которого нет бесконечных убывающих цепочек элементов. Стандартное определение немного отличается, но для наших множеств (заведомо счётных, с другими даже идеальные Тьюринг-полные компьютеры не умеют работать) разница невелика и без аксиомы выбора. В качестве синонима в конструктивных контекстах часто используется понятие «доступности» (или как на русский перевести «accessible» в этом контексте?), которым я тоже иногда буду пользоваться.


    Кроме того, немного про Агду, на которой мы и будем всё это писать. Это язык из ML-семейства с похожим на хаскель синтаксисом и с поддержкой зависимых типов. Стоит упомянуть пару синтаксических особенностей, которые не встречаются, пожалуй, ни в одном другом языке:


    • Агда поддерживает миксфиксные операторы — то есть, операторы с любым числом аргументов (а не только унарные и бинарные) и с аргументами в произвольных местах. Места для аргументов указываются подчёркиваниями при определении оператора: например, можно определить оператор с именем if_then_else_, и тогда конструкция if a then b else c будет эквивалентна if_then_else_ a b c (и так и определяется условный оператор в стандартной библиотеке). Или можно определить оператор _⊢_⦂_ и потом писать выражения типа a ⊢ b ⦂ c — почти как в математических статьях. Обычные бинарные операторы при этом определяются как, например, _<_.
    • Имена переменных (и других идентификаторов) могут содержать практически произвольные символы, кроме пробела. Например, <acc! — валидный идентификатор. Или x<y, или a,b, или даже Γ⊢[x↦ε]τ. Можно даже использовать эмодзи, но мы этого делать не будем.

    Это очень удобно в математическом коде.

    Если читатель кода знаком с предметной областью, конечно же. Например, можно написать let Γ⊢[x↦ε]τ = sub-Γ⊢τ-head εδ Γ,x⦂σ⊢τ и получить самодокументируемое имя переменной Γ⊢[x↦ε]τ — достаточно одного взгляда, чтобы вспомнить, что в ней лежит доказательство того, что в контексте Γ выводим тип, который получился из типа τ заменой переменной x на ε. Или можно объявить функцию с именем Γ⊢ε⦂τ-⇒-Γok, которая доказывает, что из утверждения Γ ⊢ ε ⦂ τ следует утверждение Γ ok. Как это написать обычными словами в обычном языке, я не знаю. Какое-нибудь termWellformedInContextImpliesContextWellformed?


    Ещё я иногда буду писать слово «свидетель утверждения X», обозначая этим терм, имеющий тип, соответствующий утверждению X.


    Расковыриваем НОД


    Один из классических примеров, на котором ломаются стандартные termination checker'ы — алгоритм Евклида для нахождения наибольшего общего делителя двух чисел. При этом он достаточно прост для того, чтобы не тратить внимание на неважные детали, да и, оказывается, в стандартной библиотеке Агды он уже реализован. Нас интересует, в частности, вот эта функция:

    Здесь и дальше я буду приводить код в виде скриншотов, так как Хабр не умеет в раскрашивание Агды (что объяснимо, без запросов к тайпчекеру там не разберёшься), да и весь нужный уникод не у всех есть.


    Эта функция принимает два числа, доказательство, что одно из них меньше другого, и ещё какой-то параметр типа Acc _<_ m. Судя по всему, именно он отвечает за убеждение termination checker'а в завершимости функции. Но что это за Acc?


    Если мы пройдём по цепочке импортов, то увидим, что Acc определён так:



    Похоже, у нас тут полиморфизм по уровням вселенных (или как там по-русски «universe levels»?) со всеми этими a и , но для развития интуиции мы можем их просто проигнорировать и считать, что мы работаем в нашей обычной вселенной обычных типов. Ну или, по крайней мере, лично мне так удобно делать — меньше вещей нужно держать в голове.


    Кроме того, Acc параметризован:


    • некоторым типом A (который мы далее будем считать фиксированным),
    • отношением _<_ (если забыть про вселенные, то это просто функция A → A → Set),
    • и элементом x типа A.

    С типом и отношением всё понятно — в конце концов, мы говорили про «меньше», то есть, про какое-то отношение, и это отношения являются фундированными, гарантируя отсутствие бесконечных цепочек вызовов, так что они обязаны были где-то вылезти. А вот причём здесь x, непонятно, так что давайте посмотрим, как он используется в единственном конструкторе acc типа Acc.


    Конструктор упоминает какой-то WfRec, который определён так:



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


    Для любопытствующих.

    Пожалуй, смысл этих типов можно было бы понять из контекста, но давайте не будем жульничать и посмотрим на определения.


    Rel использует более общий REL, но в итоге, как и ожидалось, всё сводится к функции A → A → Set:



    С RecStruct всё чуть сложнее:



    Комментарий ссылается на модуль Induction.Nat, который устарел и был распилен на модули, а более новый Data.Nat.Induction не особо богат на примеры. Щито поделать.


    В любом случае, если пристально посмотреть на это определение, то станет ясно, что RecStruct принимает тип A и возвращает какой-то другой тип — функцию из Pred A в себя же, а Pred A по большому счёту является функцией A → Set — как и положено всякому благочестивому предикату в теории типов.


    Получается, что RecStruct A — это (A → Set) → (A → Set), и Rel A — это A → A → Set. С учётом этого, если мы раскроем WfRec в определении Acc, то получим:



    Становится понятнее. Чтобы создать значение типа Acc _<_ x, мы должны предоставить функцию, которая для любого y, меньшего x согласно отношению _<_, может создать Acc _<_ y.


    Но как это вообще связано с завершимостью? Почему этого Acc достаточно, чтобы доказать, что что-то завершается?


    Доступность и структурная рекурсия


    Оказывается, что это наша старая добрая структурная рекурсия под прикрытием.


    В структурной рекурсии всё в порядке, если, сильно упрощая, мы совершаем рекурсивный вызов на синтаксическом субтерме одного из наших термов-аргументов. Вот, например, привычный Фибоначчи:



    В последней строчке рекурсивный вызов происходит либо с n, либо с suc n, и оба эти терма прямо синтаксически являются кусочками терма-аргумента suc (suc n). Метатеории всех наших любимых зависимо типизированных языков гарантируют, что все значения любого типа данных «конечны», поэтому эта функция рано или поздно завершится.


    В Фибоначчи используется один из самых простых типов данных в мире, тип натуральных чисел:



    но такая же логика работает и для чего-нибудь более сложного. Например, для бинарных деревьев:



    Рекурсивные вызовы на каждом из поддеревьев, естественно, вполне себе корректны и доказуемо завершимы:



    А теперь время для ключевого трюка. Заметим, что определение Tree выше изоморфно такому:



    Действительно, наш исходный конструктор node содержит два поддерева. Наш новый node' тоже содержит два поддерева, просто в виде функции, которая возвращает, например, левое поддерево, если ей передать true, и правое — если false (фанаты монады Either могут всё сделать наоборот):



    Аналогично можно поступить и с натуральными числами, просто в этом случае функция будет принимать аргумент типа, содержащего всего одно значение:



    Упражнение для читателя: напишите функцию-свидетель изоморфизма между Tree и Tree'. Напишите функцию-доказательство, что функция-свидетель на самом деле является изоморфизмом.


    Но, если Tree и Tree' изоморфны, то можно ожидать, что termination checker посчитает функцию countBiased' с последнего листинга завершающейся точно так же, как он считает завершающейся функцию countBiased. И, к счастью, это действительно так!


    Подход Tree' и ℕ' выглядит более тяжеловесно и неуклюже, чем привычный способ описания типов, но у него есть два преимущества. Во-первых, этот подход хорошо обобщается и куда более выразителен. Например, можно представить себе дерево со счётно бесконечным числом поддеревьев в каждом узле:



    Или дерево, где в каждом узле конечное, но неизвестное заранее число поддеревьев:



    Во-вторых, возвращаемые значения функций, «хранящихся» в конструкторах, считаются termination checker'ом структурно меньшими, так что мы спокойно можем делать рекурсивные вызовы на этих возвращаемых значениях (и метатеория языка гарантирует, что это на самом деле всё ещё консистентно). Например, можно написать что-то в духе подсчёта глубины «диагонали» дерева с бесконечным числом детей в каждом узле:



    Визуализировать эту функцию уже не так просто, как написать, но написать можно, и termination checker вполне корректно будет считать её тотальной.


    Если вернуться к нашим НОДам, то можно заметить, что Acc имеет примерно ту же форму, что и все эти забавные типы, описанные выше. В частности, конструктор Acc _<_ x принимает функцию, которая по элементу y и свидетелю y < x возвращает другой Acc (конкретнее, значение типа Acc _<_ y). Теперь мы знаем, что termination checker считает этот Acc _<_ y как структурно меньший, чем исходный Acc _<_ x (кстати, даже несмотря на то, что его тип отличается). Поэтому мы можем передать это новое значение в рекурсивный вызов, и termination checker с удовольствием посчитает это корректной завершимой рекурсией, даже если ни один из прочих аргументов не стал структурно меньше.


    В каком-то смысле Acc позволяет преобразовать «меньше-согласно-отношению» в «структурно-меньше», и нам, программистам, остаётся заполнить пробелы в этом преобразовании.


    Примеры


    Но как именно выглядит это преобразование?


    Натуральные числа


    Давайте для начала напишем доказательство того, что каждое натуральное x «доступно» (Acc — сокращение от «accessible») согласно обычному отношению «меньше-чем». Мы будем использовать отношение _<′_ из модуля Data.Nat.Base, которое эквивалентно _<_, но чуть более удобно в этом контексте.


    Это доказательство — просто объект типа Acc _<′_ x для любого x:



    После обычных для Агды пасов мы придём к чему-то вроде такого:



    Давайте сосредоточимся на f. Как заполнить эту дырку? Если есть сомнения, делай case split! Так что давайте сделаем split по доказательству y<′x:



    Теперь первая дырка ожидает от нас некое значение типа Acc _<′_ y. Но вот что интересно: наша функция верхнего уровня, которую мы пишем, <′x-acc, возвращает ровно это значение, если ей передать y! Кроме того, такой рекурсивный вызов вполне удовлетворит наш termination checker, так как даже в худшем случае отсутствия прямого рекурсивного вызова f из f (который появится во второй дырке, которую мы заполним позже), y будет субтермом suc y, который равен x, переданному в изначальный вызов f и являющемуся формальным параметром <′x-acc. Короче, можно заполнить первую дырку как <′x-acc y.


    Если теперь перейти ко второй дырке, убрать dot pattern и дать имя первому аргументу, то получим что-то такое:



    В дырке при этом будет такая цель и такой контекст:


    Goal : Acc _<′_ y
    --------------------------------------------------------------------------------
    x : ℕ
    y : ℕ
    y<′x : y <′ x

    Тут прямо напрашивается рекурсивный вызов f с передачей x, y и y<′x. Легко видеть, что результат рекурсивного вызова будет иметь нужный тип, и Агда с нами согласится. Итого, такое определение корректно и тотально:



    Пары чисел


    Что насчёт чего-нибудь более сложного, как, например, пар натуральных чисел с лексикографическим порядком?


    Такой порядок можно определить, например, так:



    Доказательство его фундированности предлагается читателю в качестве упражнения.


    Ладно, шучу, мне просто лень описывать процесс разработки доказательства. Конечный результат будет выглядеть примерно так:



    Можно заметить, что доказательство имеет примерно ту же структуру: мы рекурсивно вызываем нашу основную функцию <,<acc в случае ≤′-refl (так как мы стали меньше), а в остальных случаях мы рекурсивно вызываем нашу вспомогательную функцию f.


    Контрпримеры


    Итак, мы встретились с парой типов и отношений на них, а также доказали их вполне упорядоченность. Но что случится, если мы попытаемся доказать что-то про фундированность отношения, которое таковым не является? Где именно и что именно сломается? Доказывать, что какие-то вещи невыразимы, бывает сложно, но мы попытаемся хотя бы немножко приблизиться к интуитивному пониманию этой самой невыразимости. Да и лично я считаю, что контрпримеры так же важны для понимания, как и обычные, положительные примеры, так что давайте ломать!


    Тривиальный тип


    Пожалуй, самый простой пример — тип-синглтон с отношением, которое выполняется для любых двух элементов этого типа (тривиальным образом, так как у этого типа всего один элемент):



    Давайте начнём писать доказательство фундированности:



    Каков тип этой дырки?


    Goal : Acc _!_ x
    --------------------------------------------------------------------------------
    x : ⊤

    Единственный способ создать значение типа Acc — через конструктор acc:



    Здесь y!x — свидетель отношений между y и x. Но этот свидетель не даёт нам никакой новой информации, так как мы и так знаем, что любое значение связано с любым, поэтому мы можем его просто проигнорировать!



    Какой тип дырки перед нами после этого?


    Goal : Acc _!_ y
    --------------------------------------------------------------------------------
    x : ⊤
    y : ⊤

    Похоже, что мы пришли к тому, с чего начали: нам нужно произвести некоторый Acc _!_ y для y, о котором мы ничего не знаем, и нам только остаётся ещё раз воспользоваться конструктором acc, передав в него ещё одну лямбду, и так до бесконечности. Понятно, что записать это не получится.


    Ходим кругами


    Что насчёт чего-нибудь поинтереснее? Давайте поиграем в камень-ножницы-бумагу, также известные как числа Пеано без аксиомы ∀x. suc(x) ≠ 0 на трёхэлементном множестве:



    Из-за конечности Obj представляется разумным попытаться доказать фундированность через case split по аргументу. Затем давайте рассмотрим произвольную ветку после сплита (я люблю метал, поэтому выберу rock):



    Если мы теперь сделаем сплит по y<x, то получим



    с целью Acc _<_ scissors. Но мы не можем её заполнить ни через <acc scissors (termination checker'у это не понравится), ни через ручное разворачивание дырки на манер того, как мы делали раньше — через пару итераций такого разворачивания мы придём к необходимости снова произвести значение типа Acc _<_ rock без какой-либо дополнительной информации — то есть, снова придём к тому, с чего начали.


    Бесконечные цепи уникальных элементов


    Если мы вернёмся к натуральным числам, но теперь рассмотрим отношение _>_ «быть больше, чем», то у нас тоже не получится доказать его фундированность. Неформально говоря, дело в том, что для любого наперёд заданного x нам может быть дано число y, большее, чем x, для которого нужно предоставить свидетеля фундированности. Для этого y тоже может быть дано третье число z, большее, чем y. Но проблема в том, что чисел, больших, чем x, столько же, сколько чисел, больших чем y, так что мы никак не сузили наше «целевое пространство»!


    Или, другими словами, пусть у нас есть такой свидетель. Тогда мы можем скормить ему 0, заем 1, затем 2, и так далее. Так как мы по факту имеем структурную рекурсию, то мы сможем написать незавершающееся вычисление, но, так как Агда консистентна, этого не может быть!


    Или, в виде кода, кратко и ясно:



    Так что либо ℕ не населено (что, очевидно, не так), либо Acc _>_ x не населён для любого x.


    Наконец-то рекурсия


    Как же используется доказательство фундированности? Посмотрим ещё раз на функцию вычисления НОД:



    Во втором случае мы знаем, что второй аргумент n меньше первого аргумента m. Из достаточно простой арифметики следует, что остаток от деления m на n меньше n, так что рекурсивный вызов происходит с корректными первыми двумя аргументами, а последний аргумент использует некую лемму m%n<n%, обосновывающую арифметические соображения, на которые я сейчас сослался. В третьем же аргументе мы пользуемся свидетелем доступности, возвращаемым rec для числа n (которое, как мы помним, меньше, чем m). Termination checker всем доволен по ровно тем же причинам, как и в случае diagCount выше.


    Заключение


    После этого маленького экскурса у меня получилось написать что-то чуть менее тривиальное, с кучей взаимно рекурсивных функций, бегающих по взаимно рекурсивным деревьям вывода в системе типов, формализацией которой я сейчас занимаюсь. Надеюсь, что если тебе, дорогой читатель, понадобится доказуемо завершимая рекурсия, эти записи помогут тебе с ней разобраться. Тем более, что, на мой взгляд, чаще всего все доказательства завершимости сводятся к введению размера как прямого отображения на множество натуральных чисел, а там с фундированностью всё просто, и 640 килобайт Acc _<_ хватит всем.


    Кроме того, похожие фичи есть и в Idris в виде accInd/accRec и обёрток sizeInd/sizeRec для того самого случая размера как натурального числа. Да и, учитывая, что мы разобрали, как определяется и как работает Acc, не составит труда определить самостоятельно соответствующий примитив в любом зависимо типизированном языке.

    AdBlock похитил этот баннер, но баннеры не зубы — отрастут

    Подробнее
    Реклама

    Комментарии 92

      +6

      Удивительно простое и незагаженное лишней сложностью изложение.

        +3

        Немного не по содержанию вопрос: А как вы эти юникодовые символы набираете в вашем редакторе Агды?

          +4

          Там специальные мнемоники есть, которые редактор преобразует в символы. Например, для \mapsto, \|-, \top, \bot. Они, в принципе, логичны, и наборы символов из одной категории набираются похоже. Например, \bN, и прочие blackboard-символы — через \b<буква>. α\Ga (и прочие греческие через \G<буква>). Стрелочки всякие — по направлению стрелки и её виду, типа, \d для (потому что down), \r~ для , \ur (upper right?) для стрелки вправо вверх (которую здешний редактор почему-то проглатывает).

            +2
            Чем-то сильно отдалённо напоминает LaTeX… и клавишу compose в иксах.
          0

          Я правильно понимаю, что без доказательства завершимости программа не компилируется?
          Как при этом выглядит ошибка?


          Сколько времени заняла постановка проблемы и весь этот процесс решения?

            +4
            Я правильно понимаю, что без доказательства завершимости программа не компилируется?

            Да, если не указать тем или иным образом, что для данной конкретной функции проверка завершимости не требуется.


            В идрисе, кстати, это состояние по умолчанию (он больше на продакшен ориентирован, а не на доказательство теорем), и там, наоборот, надо явным образом либо просить проверку завершимости отдельных функций (для этого есть ключевое слово total, которым эти функции надо помечать), либо менять это умолчание для модуля целиком (через прагму %default total).


            Как при этом выглядит ошибка?

            Для рассматриваемой функции gcd, например, если убрать Acc-параметр, будет


            Test.agda:22,1-24,54
            Termination checking failed for the following functions:
              gcd′
            Problematic calls:
              gcd′ (suc n-1) (m % suc n-1) (m%n<n m n-1)
                (at Test.agda:24,26-30)

            В моей конкретной задаче было


            так
            /home/d34df00d/Programming/refinedt-temp/agda/Surface/Theorems/Thinning.agda:14,3-46,45
            Termination checking failed for the following functions:
              twf-thinning, t-thinning
            Problematic calls:
              t-thinning (PrependBoth ⊂-prf) (TCTX-Bind Γ'ok (TWF-TrueRef Γ'ok))
              ε₂δ
                (at /home/d34df00d/Programming/refinedt-temp/agda/Surface/Theorems/Thinning.agda:19,108-118)
              twf-thinning ⊂-prf Γ'ok arrδ
                (at /home/d34df00d/Programming/refinedt-temp/agda/Surface/Theorems/Thinning.agda:32,58-70)
              thin-branches branches
                (at /home/d34df00d/Programming/refinedt-temp/agda/Surface/Theorems/Thinning.agda:37,134-147)
              twf-thinning ⊂-prf Γ'ok (Γok-head (Γ⊢ε⦂τ-implies-Γok εδ))
                (at /home/d34df00d/Programming/refinedt-temp/agda/Surface/Theorems/Thinning.agda:43,44-56)

            То есть, в принципе, можно даже восстановить последовательность вызовов и понять, что именно чекеру не нравится.


            У идриса сообщения


            чуть другие
            Error: size is not total, possibly not terminating due to recursive
            path Main.size -> Main.Sized implementation at Test.idr:70:3--74:17 -> Main.size -> Main.Sized implementation at Test.idr:74:3--84:17 -> Main.size -> Main.Sized implementation at Test.idr:70:3--74:17 -> Main.size -> Main.Sized implementation at Test.idr:74:3--84:17 -> Main.size -> Main.Sized implementation at Test.idr:84:3--90:1 -> Main.size -> Main.Sized implementation at Test.idr:70:3--74:17 -> Main.size -> Main.Sized implementation at Test.idr:74:3--84:17 -> Main.size -> Main.Sized implementation at Test.idr:84:3--90:1 -> Main.size -> Main.size -> Main.Sized implementation at Test.idr:74:3--84:17 -> Main.size -> Main.Sized implementation at Test.idr:84:3--90:1 -> Main.size -> Main.Sized implementation at Test.idr:70:3--74:17 -> Main.size
            
            Test.idr:84:3--90:1
             84 |   implementation Sized (T g e t) where
             85 |     size eprf = S $ case eprf of
             86 |                          T_Unit gok => size gok
             87 |                          T_Var gok _ => size gok
             88 |                          T_Abs arrTy bodyTy => size arrTy + size bodyTy
             89 |                          T_App funTy argTy => size funTy + size argTy
            
            Error: size is not total, possibly not terminating due to call to Main.size
            
            Test.idr:74:3--84:17
             74 |   implementation Sized (TWF g t) where
             75 |     size typrf = S $ case typrf of
             76 |                           TWF_TrueRef gok => size gok
             77 |                           TWF_Base e1deriv e2deriv => size e1deriv + size e2deriv
             78 |                           TWF_Arr argDeriv resDeriv => size argDeriv + size resDeriv
             79 |       where
            
            Error: size is not total, possibly not terminating due to call to Main.size
            
            Test.idr:70:3--74:17
             70 |   implementation Sized (TCTX g) where
             71 |     size TCTX_Empty = 0
             72 |     size (TCTX_Bind prevOk tyPrf) = S (size prevOk + size tyPrf)
             73 | 
             74 |   implementation Sized (TWF g t) where
            
            Error: size,go is not total, possibly not terminating due to call to Main.size
            
            Test.idr:80:9--81:11
             80 |         go : All (\conTy => TWF g conTy) cons -> Nat
             81 |         go [] = 0

            Сколько времени заняла постановка проблемы и весь этот процесс решения?

            Сложно сказать. Разобраться с тем, как оно работает в агде и поиграться с разными примерами — часов 6 (из которых я дольше, чем нужно, потратил на доказательство фундированности обычного отношения _<_ на натуральных числах, которое определено не очень дружественно к этой задаче). Знать что-то про фундированные множества, про доказуемую завершимость, про strong normalization property всяких разных систем типов — фиг знает сколько часов когда-то давно.


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

            +5
            Я понял что для доказательства завершимости рекурсии один из аргументов должен принадлежать частично упорядоченному множеству и все время убывать. Я не понял, в какой момент мы доказываем, что это множество содержит минимальный элемент. Или это явно следует из конструирования типов?

            Откуда мы знаем что Acc _<_ x «конструктивно меньше» чем Acc _<_ y, если y < x?
              +4

              Отличный вопрос!


              Откуда мы знаем что Acc _<_ x «конструктивно меньше» чем Acc _<_ y, если y < x?

              Мы это не знаем: между ними нет такой связи только из-за того, что y < x (хотя, скорее всего, вы имели в виду x < y). Тут важно то, что вы берёте какой-то уже существующий у вас acc-y типа Acc _<_ y, достаёте из него функцию, производящую свидетеля для меньших x, передаёте туда конкретный x и доказательство того, что он меньше y, она там внутри крутит шестерёнками, булькает и выплёвывает вам какое-то значение типа Acc _<_ x. И вот это конкретное значение будет считаться синтаксически меньше, чем acc-y, просто по факту того, что его вернула функция, лежащая в acc-y.


              Иными словами, пусть у нас есть функция (и она на самом деле есть где-то в стандартной библиотеке агды) <-acc : (x : ℕ) → Acc _<_ x. Если вы перепишете вторую строчку gcd′, забыв про переданный вам Acc _<_ m, заменив его вайлдкардом и написав, например,


              gcd′ m n@(suc n-1) _ n<m = gcd′ n (m % n) (<-acc n) (m%n<n m n-1)

              то termination checker расстроится, хотя вы в этом случае тоже передаёте в рекурсивный вызов какое-то значение типа Acc _<_ n. Чтобы всё работало, вы должны получить это значение из функции, которая лежит в переданном вам Acc, и ниоткуда больше (интересно, есть ли тут какие-то параллели с линейной логикой?).


              Я не понял, в какой момент мы доказываем, что это множество содержит минимальный элемент.

              А мы это не доказываем. И, думаю, не можем доказать изнутри агды (или идриса, или любого другого языка) — тут уже начинает лезть всякая гёдельщина и невозможность доказать консистентность достаточной мощной логической системы из неё же (а завершимость вычислений означает консистентность). Утверждение «если нам дан тип A, отношение Rel на нём и функция f типа (x : A) → Acc Rel x, то существует x такой, что не существует y такого, что y < x» слабее, конечно же, но я не знаю, как его доказывать без опоры на завершимость функции f, а про это рассуждать изнутри агды нельзя по гёделевским причинам. Ну и ещё вы ничего не знаете про A, так что параметричность тут тоже играет роль, но в данном контексте это не столь интересно. Ну и оно не выполняется для некоторых A (возьмите bottom type, например), но это ещё менее интересно.

                0
                И вот это конкретное значение будет считаться синтаксически меньше, чем acc-y, просто по факту того, что его вернула функция, лежащая в acc-y.
                То есть, проще говоря, на примере gcd′, мы вернулись к «старой доброй структурной рекурсии» в силу того, что значение gcd' c третьим аргументом типа Acc _<_ m, выраженным как aсc rec выводится из gcd' с третьим аргументом вычисляемым из rec?

                Под «конструктивно меньше» я имел ввиду «является сабтермом». Как я понял, это должно следовать из самого определения рекурсивной функции, а не из каких-то особых свойств Acc.

                И мы точно знаем, что вереница «деконструкций» acc rec рано или поздно закончится просто в силу метафизической природы вселенной и самого факта потенциальной осуществимости изначального Acc _<_ m?
                  0
                  То есть, проще говоря, на примере gcd′, мы вернулись к «старой доброй структурной рекурсии» в силу того, что значение gcd' c третьим аргументом типа Acc < m, выраженным как aсc rec выводится из gcd' с третьим аргументом вычисляемым из rec?

                  Да.


                  Под «конструктивно меньше» я имел ввиду «является сабтермом». Как я понял, это должно следовать из определения самой рекурсивной функции, а не из каких-то особых свойств Acc.

                  Именно. И тут всё получается потому, что мы пользуемся функцией rec, которая является субтермом терма-аргумента acc rec


                  И мы точно знаем, что вереница «деконструкций» acc rec рано или поздно закончится просто в силу метафизической природы вселенной и самого факта потенциальной осуществимости изначального Acc < m?

                  Да.


                  Но это доказывается, опять же, вне агды (хотя можно на агде написать свою агду-в-агде и доказать что-то про неё, но перенос доказательства с агды-в-агде на внешнюю агду вы не сможете сделать внутри агды, для этого вам придётся включать свой, внешний относительно агды мозг, и рассуждать «извне»).


                  Посмотрите ещё diverge из (контр)примера с натуральными числами и отношением «больше» — там, если прочитать то, что записано в типе, мы предполагаем населённость натуральных чисел и соответствующего Acc и получаем боттом, а получать боттомы плохо.


                  Ну и ещё, раз уж мы тут о метатеориях заговорили, полезно упомянуть, что есть такая тема, как strict positivity, и если её отключить (как в самом низу страницы по ссылке), то можно получить боттом (или бесконечную рекурсию, или что хотите) безо всяких предположений. Это пример того, что метафизическую природу вселенной (вернее, одного конкретного языка) можно сломать, если отключить некоторые проверки. Или если включить некоторые другие вещи, но это уведёт нас сильно


                  в дебри

                  Просто скажу для затравки, что, например, кубическая теория типов, в которой доказуема аксиома унивалентности из модной нынче гомотопической теории типов и из которой прямо следует неединственность пропозиционального равенства, по очевидным причинам несовместна с аксиомой о единственности пропозиционального равенства. Хотя последняя, в свою очередь, совместна с классическими зависимыми типами в стиле реализованных «по умолчанию» в коке/агде/идрисе.


                  Так что консистентность — это сложно.

                    +2
                    Но это доказывается, опять же, вне агды...
                    Да, этот момент мне ясен, я хотел убедиться что правильно понимаю где мы упираемся в свойства агды, когда гарантируем завершимость не тривиальных рекурсивных функций.

                    Как человек, который написал только пару строк на idris и ни строки на agde и coq, я рад что многое понял из статьи!

                    Можете еще объяснить момент с выведением <‘x-acc? (Хотя я думаю что он имеет в в большей степени отношение к самой agda, а не топику статьи).

                    Какие взаимоотношения между <' и ≤’-refl/≤’-step? Откуда и почему они возникают в определении?
                      +1
                      Какие взаимоотношения между <' и ≤’-refl/≤’-step? Откуда и почему они возникают в определении?

                      А, да, мне стоило про это написать, конечно. Это конструкторы отношения _≤’_, а _<’_ определяется через _≤’_:


                      data _≤′_ (m : ℕ) : ℕ → Set where
                        ≤′-refl :                         m ≤′ m
                        ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
                      
                      _<′_ : Rel ℕ 0ℓ
                      m <′ n = suc m ≤′ n

                      Чуть позже добавлю это в статью.

              +1
              Согласен, статья годная.

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

              Но главный плюс — похоже, я всерьёз заинтересовался Agda.
                –1

                Ничего не понял, но у меня пара вопросов по Агде:


                • Выразима ли в ней четырёхзначная логика?
                • Выразима ли в ней релевантная имликация?
                  0
                  Выразима ли в ней релевантная имликация?

                  А что это такое, "релевантная имликация"? Что-то по этим ключевым словам гуглятся только статьи каких-то гуманитариев, которые до сих пор думают, будто логика изучает "единички" и "нолики", а не утверждения в символьном виде...

                      +1

                      Тем, что ведет на статью в гуманитарной энциклопедии, лежащую на гуманитарном портале, в которой за наукообразными словами не видно смысла.

                      +2

                      Я там тоже ничего не понял.


                      Разве что, в очередной раз понял, что ничего не понимаю в математике, потому что


                      известным парадоксам материальной импликации A → (B → A) и A → (¬ A → B)

                      эти парадоксы для меня неизвестны, вернее, неизвестна парадоксальность этих тавтологий. Вам же не кажется парадоксальной функция fst : a -> b -> a? И да, я помню о видео, которое вы кидали в другом треде, но видео я не очень люблю смотреть, и до него ещё руки не дошли.


                      И да, у меня тоже сложилось такое чувство, что туда накидали побольше всяких умно звучащих слов, но вот смысл туда вложить забыли.

                          +3

                          Да, вы давали эту ссылку в прошлый раз. Я всё ещё не вижу парадоксов с точки зрения математики.


                          Этой импликацией можно связывать только те утверждения, которые имеют общее содержание.

                          Как формализуется понятие общего содержания?

                            0

                            Пример с дедукцией может выглядеть как-то так:


                            ! x isPartOf Y =>( isMy Y => isMy X ) // связка предикатов
                            ! theDoor isPartOf theHouse // связка объектов
                            ? isMy theHouse => isMy theDoor // истина
                              0

                              Я скорее имел что-то в духе formation rule для высказываний этой логики. Ну или хотя бы описание семантики.

                                0

                                Если интуитивно, то единственная вменяемая интерпретация, это что у них там a -> b, если из а можно вывести b и а "несократимо".

                                  0

                                  Насколько несократимо? Я могу любую несократимую предпосылку объединить с любой другой иррелевантной посылкой конъюнкцией и получить аналог «парадоксов» по ссылке где-то здесь. Но если запретить такие объединения, то a /\ b → a в этой логике не выполняется, а это ерунда какая-то, я не понимаю, что с ней делать.

                                    0
                                    Я могу любую несократимую предпосылку объединить с любой другой иррелевантной посылкой конъюнкцией

                                    И тогда она станет сократима, очевидно.


                                    В общем, выбираем некую ф-ю f, которая каждому утверждению Х ставит в соответствие множество утверждений f(X), такое, что:


                                    1. ни одно из f(X) невыводимо (по правилам классической логики) из остальных
                                    2. конъюнкция всех f(X) тождественна (в классической логике) X
                                      Назовем такую f, например, сепулькой.

                                    Логику будем называть релевантной относительно сепульки f, если в ней a -> b тогда и только тогда, когда b выводимо (по правилам классической логики) из f(a), но невыводимо из строгих подмножеств f(a).


                                    Ну а дальше дело за определением конкретных сепулек. Как их выбираем? По интересности, очевидно, если какая-то сепулька дает какую-то содержательную теорию — можно ее рассматривать.
                                    В простейшем случае f(x) = {x} получаем классическую логику.

                          0

                          Проблема в том, что, насколько я понял, "парадоксы материальной импликации" не являются парадоксами с точки зрения строгой теории. Это скорее ближе к парадоксу удвоения шара — вполне строгий математический результат (пусть и без конструктивного доказательства), который при этом не вписывается в наглядное понимание соответствующей математики.


                          upd: собственно, раз нам кинули ссылку на Википедию, цитирую соответствующую английскую статью:


                          The paradoxes of material implication are a group of formulae that are truths of classical logic but are intuitively problematic.

                          (выделение моё)

                            0

                            Суть парадокса в том, что материальная импликация не годится для выражения причинной связи, но при этом часто используется именно для этого, ибо в классической логике нет способа выразить причинную связь. В результате чего играться с битами она позволяет, а вот делать корректные выводы — нет.

                              +1
                              в классической логике нет способа выразить причинную связь

                              Естественно. В любой строгой теории, если её рассматривать в отрыве от моделируемой части реального мира, неизбежно будут подобного рода "провалы".

                                –1

                                В том-то и дело, что классическая логика моделирует скорее часть нереального мира, где выражения в духе "1>2 => 2<3" истинно.

                                  +1

                                  Но приведённое вами выражение и правда истинно, доказываясь в два шага (сначала добавляем 1 к обоим числам, потом "разворачиваем" сравнение).


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

                                    –1

                                    Внимательно прочитайте, прежде чем огульно минусовать.


                                    А мат доказательства в основном основываются не на импликации, а на правилах вывода, которые базируются уже (внезапно) на интуитивном понимании причинной связи (дедукция, индукция и вот это всё).

                                      0

                                      А, ну да, для 2<3 понадобится ещё шажок.


                                      А мат доказательства в основном основываются не на импликации, а на правилах вывода

                                      Ага, но как только импликация перестаёт выполняться для правил вывода — она перестаёт быть импликацией и превращается в какую-то чушь.

                                        +3
                                        А мат доказательства в основном основываются не на импликации, а на правилах вывода, которые базируются уже (внезапно) на интуитивном понимании причинной связи (дедукция, индукция и вот это всё).

                                        Нет, это не так. Интуитивные доказательства из математики стали пропадать очень давно, и окончательно пропали лет 100-150 назад.


                                        Да и в тех же правилах вывода вполне выводим (и населён) тип a -> b -> a, который так близок так не нравящимся вам «парадоксам» импликации.


                                        А что до вашего примера — его можно доказать даже в релевантной импликации (которую я для себя решил моделировать линейной логикой, в которой я, впрочем, ничего не понимаю). Если 1 > 2, то 2 > 2 (потому что если a > b, то suc a > b — звучит интуитивно, не так ли?), но тогда и 3 > 2. Что же делать?

                                          0

                                          Речь не о доказательствах, а о правилах вывода. Они задаются интуитивно. Так же как и аксиомы.


                                          2<3 можете заменить на 2*2=4 — суть проблемы не поменяется.

                                            0
                                            Речь не о доказательствах, а о правилах вывода. Они задаются интуитивно.

                                            Интуитивные правила вывода есть только в natural deduction, а это далеко не единственный (и даже не самый удобный) формализм. Что интуитивного в списке из 11 аксиом в стиле Гильберта?


                                            (1) A → (B → A);
                                            (2) (A → (B → C)) → ((A → B) → (A → C));
                                            (3) (A ∧ B) → A;
                                            (4) (A ∧ B) → B;
                                            (5) A → (B → (A ∧ B));
                                            (6) A → (A ∨ B);
                                            (7) B → (A ∨ B);
                                            (8) (A → C) → ((B → C) → (A ∨ B → C));
                                            (9) ¬A → (A → B);
                                            (10) (A → B) → ((A → ¬B) → ¬A);
                                            (11) A ∨ ¬A.
                                              0

                                              Думаете Гильберту эти аксиомы приснились? Формируются они примерно так: "жопой чую, что это так, но доказать не могу, поэтому пусть будет аксиомой".

                                                +1

                                                А, то есть, «жопой чую, что A → (B → A)»? Тогда какие вопросы к интуиции?


                                                А вообще они формируются так, что первые две аксиомы позволяют доказать лемму о дедукции (что A ⊢ B эквивалентно ⊢ A ⇒ B), следующие три специализируют поведение конъюнкции (тут прям видно два элиминатора и один интродьюсер из натуральной дедукции), следующие три — поведение дизъюнкции (два интродьюсера и один элиминатор), дальше поведение отрицания, ну и аксиома исключённого третьего.


                                                Ну и это же не единственный вариант. Я вчера работал с другой системой аксиом, и там доказать A ⇒ A лично у меня уже не получилось, например (зато получилось у прувера, в который чувак, отвечавший на мой вопрос, загнал эту систему аксиом).

                                                  –1

                                                  Вы что доказать-то этими инсинуациями пытаетесь? То, что среди разумных аксиом затесалась глупая, лишь свидетельствует об интуитивности их введения.


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

                                                    +5
                                                    Вы что доказать-то этими инсинуациями пытаетесь? То, что среди разумных аксиом затесалась глупая, лишь свидетельствует об интуитивности их введения.

                                                    Я пытаюсь выяснить для себя вашу позицию, потому что я совсем перестал понимать, что вы имеете в виду под интуитивностью, парадоксами, и, более того, какую проблему вы вообще пытаетесь решить. Сначала оказывается, что A → (B → A) не понятна интуитивно, потом её наличие оказывается интуитивно понятным. Щито? Как это сочетается?


                                                    Вы вот развели нерелевантный срач, а на на оба мои исходных вопроса так и не ответили.

                                                    Потому что я так и не понял, что за релевантная импликация.


                                                    А от этого зависит буду ли я копать Агду или же придётся пилить свой инструментарий.

                                                    Я бы в любом случае пилил свой, потому что велосипеды — это весело и познавательно.

                                                      0

                                                      Хоть я в целом и не согласен с nin-jin, но выбор аксиом мне и правда не кажется формализуемым, просто потому что у нас во-первых есть интуиты против контсруктивистов и все вот это, с разным набором аксиом и т.п. Стоит ли добавлять аксиому выбора или нет? В какой момент добавление или НЕ добавление такой аксиомы это бред? Вон цитируя ту же википедию


                                                      img


                                                      Или модус поненс: почему правило вывода именно такое? У меня нет ответа кроме "ну, оно кажетися интуитивно правильным".

                                                        +1
                                                        Хоть я в целом и не согласен с nin-jin, но выбор аксиом мне и правда не кажется формализуемым

                                                        Абсолютно верно, он не формализуем (и нифига не интуитивен).


                                                        В какой момент добавление или НЕ добавление такой аксиомы это бред?

                                                        Бред — как только делает систему unsound. Ну даже не то чтобы бред, просто пользы от такой логической системы становится мало.


                                                        Или модус поненс: почему правило вывода именно такое? У меня нет ответа кроме "ну, оно кажетися интуитивно правильным".

                                                        Потому что оно не делает систему непротиворечивой. Ну и потому что таблица истинности импликации такая: если мы знаем, что A ⇒ B равно 1, и A равно 1, то из таблицы следует, что B равно 1. Чему ещё оно может быть равно?


                                                        Аналогично можно добавить правило вывода «если мы вывели A \/ B и вывели не A, то мы можем вывести B» — но нам это не нужно, это вполне следует из аксиом и правила MP. А вот аналогичным образом заменить MP не получится.


                                                        Если проводить параллели со всякими хаскелями-идрисами, то набор аксиом описывает набор базовых доступных термов, а MP описывает их вычислительное поведение.


                                                        Стоит ли добавлять аксиому выбора или нет?

                                                        Ну это аксиома немного другого рода.


                                                        Это, кстати, напомнило мне довольно любопытный, на мой взгляд, вопрос. В логике первого порядка есть такая штука, как теорема о компакте, говорящая, что если у любого конечного подмножества утверждений теории есть модель, то и у всей теории есть модель. Из неё довольно просто следует, в частности, что любое множество можно вполне упорядочить (просто рассматриваем произвольные конечные его подмножества, которые упорядочиваются тривиально), и мы получаем её эквивалентность аксиоме выбора. Известное мне доказательство опирается на теорему Гёделя о полноте (доказательство которой неудобно и тяжеловесно, но на самом деле просто). Вопрос: где в логике первого порядка «зашита» аксиома выбора?

                                                          0
                                                          Если проводить параллели со всякими хаскелями-идрисами, то набор аксиом описывает набор базовых доступных термов, а MP описывает их вычислительное поведение.

                                                          Но только вычислительное поведение у нас в разных языках бывает разное, а кроме MP я знаю разве что правило генерализации, которое вроде дополняет логику кванторами, а не меняет MP


                                                          Вопрос: где в логике первого порядка «зашита» аксиома выбора?

                                                          Любопытно) Хотя все равно надо освежить знания, про модели, интерпретации и прочее. Забыл уже всё за ненадобностью :/

                                              +1
                                              2<3 можете заменить на 2*2=4 — суть проблемы не поменяется.

                                              А, и да, до меня только что дошло: не хочу заменять. Если эта ваша логическая система с её релевантной импликацией претендует на то, чтобы каким-то образом запрещать такие следствия, то она должна с равным успехом запретить что 2 < 1 ⇒ 2 < 3, что 2 < 1 ⇒ 2 * 2 = 4. И теперь мне очень интересно, как сформулировать логику, которая бы запретила приведённое выше рассуждение.

                                                –1

                                                Релевантная логика — не моё изобретение. Если интересно — лучше почитать соответствующие книги, чем ждать от меня пересказа.

                                                  +2

                                                  А какие книги стоит почитать? А то по приведённой вами рядом ссылке ничего не понятно.


                                                  Ну и, кроме того, лично я всё же стараюсь рассказывать про то, что знаю, а не просто отсылать к книгам.

                                                    –1

                                                    Не знаю, я планирую эту почитать.

                                                      0

                                                      Судя по первым страницам эта книжка про философскую логику. Поэтому с математиками вы скорее всего не найдете общего языка, у них другое представление о предмете. Если только вам не удастся это запрограммировать, переведя текст из слов на формальный язык.

                                                        –2

                                                        Вы всегда судите о книге по первым страницам введения даже не пролистнув остальные?

                                                          0

                                                          В качестве первичного фильтра — да, всегда. В мире слишком много книг чтобы читать все подряд.

                                                            –3

                                                            Удобное оправдание, чтобы нести любую чушь.
                                                            А подменили понятие "пролистнуть" на "прочитать" вы тоже от сильного экономия времени?

                                          0
                                          Но приведённое вами выражение и правда истинно, доказываясь в два шага (сначала добавляем 1 к обоим числам, потом "разворачиваем" сравнение).

                                          Не понял, кого куда и зачем разворачиваем, и почему истинно? Как это сработает на языке завтипов, когда каждое утверждение нужно предоставить конструктивно, в том числе "1>2".

                                            0

                                            Истинна сама импликация, а не посылка.

                                              –1

                                              Но ведь второе выражение не истина сама по себе. Т.е. надо говорить если работают такие-то аксиомы арифметики и ещё какой то мусор, то "2<3". Соответственно, это тот же случай что я доказал теорему, а потом понял что одно из условий не обязательно. Тогда я могу это условие выкинуть. Более того могло случайно оказаться что то ненужное условие ещё и было противоречиво. nin-jin никакой проблемы с интуитивным восприятием у меня нету.

                                                –1

                                                Аксиомы — на то и аксиомы, что они работают безо всяких "если".

                                                  0

                                                  Аксиомы работают, но чтобы получить утверждение про 2 и 3 надо их все же применить. Иначе как понять истинна вторая часть утвепжедния или нет?

                                          0

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

                                        +3
                                        Суть парадокса в том, что материальная импликация не годится для выражения причинной связи, но при этом часто используется именно для этого

                                        Кем, математиками?


                                        ибо в классической логике нет способа выразить причинную связь.

                                        В классической логике можно выразить теорию, в которой можно выразить причинную связь (на самом деле не совсем, но это уже вопросы следующего порядка сложности, так что фиг с ними).


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

                                        Опять же, неужто вы хотите сказать, что математика построена на шатком фундаменте, или же вы говорите про корректные выводы в бытовых рассуждениях? Последнее — это отдельный разговор, который ближе ко всяким лингвистам, наверное.


                                        В бытовых разговорах даже под «или» часто подразумевается xor, какая уж там импликация.

                                          –1

                                          Ну да, кем же ещё.


                                          Можно, так и появилась релевантная логика.


                                          Ну да, кризис оснований математики всё ещё не разрешён.


                                          Уж не хотите ли вы сказать, что в быту допустимы некорректные суждения? От того, что в русском языке дизъюнкция выражается как "и/или" правила логического вывода никак не зависят.

                                            +2
                                            Ну да, кем же ещё.

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


                                            Ну да, кризис оснований математики всё ещё не разрешён.

                                            А математики-то и не знают!


                                            Уж не хотите ли вы сказать, что в быту допустимы некорректные суждения?

                                            Я хочу сказать, что интерпретация естественных языков — не задача (мета)математики.

                                              –2

                                              Вы правда не видите разницы между корректностью интерпретаций и корректностью рассуждений?

                                                +2

                                                Надеюсь, что мы тут сейчас не о терминологии спорить начнём.


                                                Корректность рассуждений (корректное использование аксиом и правил вывода) эквивалентна (теоремы Гёделя о полноте) истинности в любой интерпретации. Поэтому разница есть, я её вижу, но она немного не в том, о чём вы, похоже, думаете.

                                                  –2

                                                  Поговорим о Гёделе, когда вы таки посмотрите видео.

                                                    +2

                                                    Боюсь, что это будет нескоро. Я из тех, кто предпочитает текстовый формат, к сожалению.

                                                    0

                                                    Уточнение: в sound (звучной?) интерпретации.

                                                      0

                                                      Я бы как «непротиворечивой» перевёл.


                                                      Впрочем, а разве бывают противоречивые (по крайней мере, для исчисления высказываний)? Это ж просто назначение булевых значений (или значений из некоторой булевой алгебры) использованным переменным.

                                                        +1

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

                                                          0
                                                          Я встречал перевод «sound» как «надёжный». Но это маргинально.
                                    +1

                                    Почему именно четырехзначная?

                                      –1

                                      А почему бы и нет?

                                        0

                                        Интересует область применения четырехзначной логики.

                                          –1

                                          Логический анализ произвольных утверждений. У классической с этим проблемы, отсюда и куча парадоксов, и основанные на них теоремы Гёделя, Тьюринга и тп.

                                        +1

                                        Потому что Корчеватель :)

                                      0
                                      Немного оффтопный вопрос, но очень хочется узнать, как у всяких agda, idris и других чистых и правильных языков обстоят дела с возможностью написания программ (тут подразумеваются библиотеки, фреймворки, инструменты) для какого-нибудь абстрактного enterprise (например можно ли относительно легко создать веб-сервис, который с одной стороны смотрит в какую-нибудь БД, а с другой стороны у него REST-like интерфейс, который отдает JSON-чики)?

                                      Для Haskell хотя бы библиотек некоторое количество присутствует, хотя при попытки собрать с десяток-другой либ в одном приложениии приходится устраивать танцы с версиями.
                                        0
                                        Немного оффтопный вопрос, но очень хочется узнать, как у всяких agda, idris и других чистых и правильных языков обстоят дела с возможностью написания программ (тут подразумеваются библиотеки, фреймворки, инструменты) для какого-нибудь абстрактного enterprise (например можно ли относительно легко создать веб-сервис, который с одной стороны смотрит в какую-нибудь БД, а с другой стороны у него REST-like интерфейс, который отдает JSON-чики)?

                                        Если вкратце, то никак. У агды, думаю, этого никогда и не будет (от неё очень пахнет доказательством теорем и хардкорным матаном, а не разработкой в прод, не та философия у языка и сообщества вокруг него). У идриса вполне может быть, он таки больше направлен на энтерпрайзное программирование, и одна из его целей — сделать юзабельный в проде язык, но пока там с этим тоже никак.


                                        Впрочем, знаю людей, которые именно поэтому для некоторых своих энтерпрайз-задач выбрали идрис, а не хаскель — не нужно спорить об экосистеме, а можно построить свою с нуля. Не уверен, что согласен с такой мотивацией, но и такое бывает.


                                        Для Haskell хотя бы библиотек некоторое количество присутствует, хотя при попытки собрать с десяток-другой либ в одном приложениии приходится устраивать танцы с версиями.

                                        Stackage LTS snapshots?

                                          0

                                          А что это за энтерпрайз задачи где нужен idris/agda/coq ?

                                            +1

                                            Те же самые задачи, только если хочется подоказывать всё =)

                                              0
                                              Ну это конечно весело но всё таки интересно, есть ли применения где эти доказательства необходимы или экономят время?
                                              Я слышал о разработках ОС где подобные языки использовались для доказательства что ОС выполняет детерминированную работу за детерминированное время, не содержит уязвимостей итд. но это очень специфичные применения, а тут мне говорят что в энтерпрайзе это тоже используют, 0xd34df00d, поделитесь примером?
                                                0
                                                Ну это конечно весело но всё таки интересно, есть ли применения где эти доказательства необходимы или экономят время?

                                                Доказательства это типы. Которые доказывают корректность. Вот если вы пишете на условной джаве потому что не хотите доказывать, что везде где передаются инты принимаются инты, а чтобы это тайпчекер делал, то проведя аналогию можете понять, зачем нужны идрисы: чтобы не писать тест что сортировка списка работает, а доказать и пусть тайпчекер проверяет это везде.

                                              +4

                                              Те конкретные люди занимались доказуемо корректными распределёнными вычислениями (в смысле всяких BOINC) с примесями крипты. Другие люди, да, например, занимались написанием ядра (которое они потом продавали) с доказуемо корректным отсутствием доступа одного процесса к памяти другого.


                                              Считать ли это всё энтерпрайзом — не знаю. Но это самое близкое, что к нему есть на практике. Да и, если честно, я не знаю, что и зачем доказывать в случае сервисов, конвертирующих JSON'ы в БД. Там тесты-то не всегда пишут, а доказательства ещё тяжелее.

                                                0
                                                Считать ли это всё энтерпрайзом — не знаю. Но это самое близкое, что к нему есть на практике. Да и, если честно, я не знаю, что и зачем доказывать в случае сервисов, конвертирующих JSON'ы в БД. Там тесты-то не всегда пишут, а доказательства ещё тяжелее.

                                                Ну мне вот очень хотелось принимать в функцию доказательство "полученный массив юзеров содержит юзеров, уникальных по полю Id" или "список координат отсортирован в порядке соответствующему движению машины".

                                              0
                                              Не все пакеты есть в LTS snapshots.
                                                0

                                                Так они тогда почти всегда спокойно прописываются в extra-deps. У меня за последние несколько лет проблемы были только, кажется, с opaleye, когда решил с ним поиграться, а его в LTS не было, и там были какие-то конфликты с версиями.

                                                  0
                                                  Раз разговор зашёл про Хаскель, не подскажите сейчас «правильнее» чем пользоваться stack или haskell platform?

                                                  ПС
                                                  Поиграться поставил себе stack.
                                                  Но плагин к IDEA, например, требует от меня haskell platform.
                                                    0
                                                    Update:
                                                    прошу прощения — всё-таки Stack нужен ((

                                                    Однако общий вопрос так и остался: какая-то тула является «рекомендуемой» (по любой причине: например более поддерживаемой \ более «идеоматической»....) или выбор полностью за пользователем?
                                                      0

                                                      Есть лагерь stack'овцев и есть лагерь пуристов-cabal'истов, которые хейтят stack по не очень понятным мне причинам. stack появился позже и решал многие проблемы cabal'а, и лично я пользуюсь stack'ом, и полёт нормальный.


                                                      В среднем со stack, имхо, меньше геморроя.

                                                      0

                                                      У меня есть stack, а haskell platform нет. IntelliJ-Haskell (я тоже последнее время пользуюсь Idea) что-то про haskell platform где-то упоминает, но оно там по факту нигде не требуется.


                                                      Лично я делаю stack new в нужной директории, а потом импортирую этот проект в Idea, и всё как-то просто работает.

                                              +3

                                              Спасибо, отичная статья! Жалко только, что в трекер мне попала достаточно поздно. В пятницу читается тяжеловато, но по крайней мере общая идея и код после тренировки идрисом более-менее читаются.


                                              После этого маленького экскурса у меня получилось написать что-то чуть менее тривиальное, с кучей взаимно рекурсивных функций, бегающих по взаимно рекурсивным деревьям вывода в системе типов, формализацией которой я сейчас занимаюсь. Надеюсь, что если тебе, дорогой читатель, понадобится доказуемо завершимая рекурсия, эти записи помогут тебе с ней разобраться.

                                              Судя по идрису на практике люди решают это хаком через fuel и


                                              partial 
                                              forever = More forever

                                              :)


                                              Кстати, видно сильное влияние английского на мышление. Та же "рекурсия под прикрытием" это прямая калька с выражения "in disguise", по русски сказали бы скорее "замаскированная". На языке вертится ещё какое-то выражение классическое прям в тему, но никак вспомнить не могу.

                                                +2
                                                Спасибо, отичная статья! Жалко только, что в трекер мне попала достаточно поздно. В пятницу читается тяжеловато, но по крайней мере общая идея и код после тренировки идрисом более-менее читаются.

                                                Спасибо! Судя по всему, вполне можно писать ещё про агду с идрисом, доказательства и вот это всё.


                                                Судя по идрису на практике люди решают это хаком через fuel

                                                Да, для практических вычислений это вполне вариант, а вот если охота таки теоремы доказывать, то получается какое-то странное следствие «то ли верно, то ли у нас топливо кончится».


                                                Кстати, видно сильное влияние английского на мышление. Та же "рекурсия под прикрытием" это прямая калька с выражения "in disguise", по русски сказали бы скорее "замаскированная".

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

                                                  0

                                                  Да, известное чувство. Со временем перестаешь пытаться искать синонимы и говорить напрямую. Со временем таки образуется брайтон-бич акцент)


                                                0
                                                Тема интересная, но, к сожалению, код практически нечитаем для тех, кто не имеет опыта с agda/idris/haskell. Выпал после второй картинки с кодом.
                                                  0

                                                  Скажу честно, тут скорее конкретно опыт агды нужен, не зря сам автор пишет, что в идрисе это было бы скорее termWellformedInContextImpliesContextWellformed вместо Γ⊢ε⦂τ-⇒-Γok.


                                                  Но без опыта идриса (выражений на тайплевеле, имплисит аргументов) действительно думаю тяжеловато.

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

                                                Самое читаемое