Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
Разворецивается всего в 600 строк Gallina. Тут прекрасно всё: и копипаста, и автоматическое именование переменных с последующим переименовыванием, и сама идея хуйнуть троекратно вложенный кейз-анализ.
> Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.
Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.
А можно ли сделать в этом вашем Coq доказательство, что всё счетно-бесконечное множество теорем, автоматически генеренных по таким-то говноправилам доказуемо стратегией, генеренной на основе конкретной теоремы?
т.е. есть генератор стратегий, ему дают теорему, он выплевывает стратегию gen_strateg(theorem) -> strategy
и есть бесконечно генерирующая теоремы херня, допустим gen_theorem(0) - одна теорема, gen_theorem(1) - другая, и так далее.
Какой тип у `стратегии'?
Вопрос я, конечно, не понял, но ответ на него скорее всего – нет. Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina). (В Lean не так, кстати. Там по слухам гомоиконность) Поэтому написать теорему про тактику в Coq – это как написать функцию, принимающую как аргумент макрос, в C.
У `стратегии' тип это список правил, по которым некая питушня что-то набрасывает в качестве пруфа теоремы, пытаясь это доказать. Ну ок, пусть будет `тактики', а не `стратегии'. Почему б не доказывать, что такие-то тактики, генерируемые на основе конкретных теорем, всегда успешно доказывают теоремы, сгенеренные таким-то способом? Т.е. доказать что генератор тактик всегда для такого семейства теорем, генерируемых таким способом, генерит такие тактики, которые всегда доказывают соотв. теорему
См. пост ниже. Ты сейчас индукцию изобрёл. Если упростить, то `теорема' – это тип, а доказательство – это терм, имеющий данный тип. И то, и другое можно параметризовать числом (т.к. в Coq нет особой разницы между типами и термами), и тогда получится твоя питушня.
Нянужно! Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь. Поэтому его используют для автоматизации, т.к. удобно.
> Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь.
Ну так почему б не написать транспилер из Ltac в Gallina? В самой Gallina сделать тьюринг-полноту с гомоиконами, и пусть само с собой там метушится, доказывая доказуемость.
Зачем? Зачем? Я могу описать функцию, принимающую стейт брейнфака возвращающую новый стейт брейнфака плюс номер шага, и через Ltac я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота. Ради чего это?
Во-первых, Ltac – логический язык, типа пролога. Формально описывать на Gallina шаг Ltac, и затем применять его с помощью Ltac – это как бутылку кваса провести через весь пищеварительный тракт наверх ко рту, чтобы вылить всё её содержимое в дыхательное горло.
> я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота
Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Чтобы доказывать применимость таких-то стратегий (стратегий, построенных по определенному шаблону) к доказыванию таких-то теорем, построенных по определенному шаблону. Сделать еще какую-то алгебру стратегий, что такие-то стратегии можно упростить, сведя их к таким-то, а вот такие стратегии это частные случаи таких стратегий. Более высокий уровень абасракции короче.
> Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Почему не будет? Так мы пробуем доказать небесконечность цикла, и раз мы так можем делать, это и есть тьюринг-полнота, мы интерпретируем брейнфак. Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?
Например, если у меня есть генератор теорем, он их генерирует бесконечное множество (теорема1, теорема2, теорема3 и так далее). Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее. И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы. Можно конечно как-нибудь обобщить само множество теорем в некую одну теорему, и сделать одну общую тактику, которая б доказывала эту одну теорему, но это как-то неправильно. Почему это не в рамках единого языка?
> Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.
Переформулировать-то можно, это понятно. Но так не выйдет доказать что-то относительно неких свойств стратегий, применимости определенных стратегий к доказыванию определенных типов теорем и так далее. Окажись стратегий частью самого языка для описания теорем, это можно было бы делать.
Тактики в Coq сугубо опциональны, и можно доказывать всё вообще без них (Agda2 братишки так и делают). Поэтому доказывать какие-то свойства про них — занятие довольно бесполезное. Есть некое подобие "стратегий", называется induction scheme. (Например: https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#rectS) Ну так это просто функция высшего порядка. Про неё да, в теории что-то можно доказать.
Но вообще, есть ли смысл доказывать нечто о том, что какие-то штуки доказываются такими-то подходами? Т.е. что если теорема (или множества теорем, которые таким-то образом механически конструируются) так-то и так-то устроена, то доказать, что доказательства, конструируемые вот по такому шаблону эту теорему (или множество теорем) будут доказывать.
В этом вроде и идея ltac. Нет никакого смысла доказывать, что он правильно работает в общем случае или для каких-то классов теорем. Достаточно просто проверять сгенерённые им пруфы для конкретных теорем которые тебе и нужно доказать.
А зачем тогда специальный язык ltac? Тогда можно и через какой-то питон пруфы кодогенерировать. Какие преимущества у ltac по сравнению с условным питоном, если его прикрутить к этому coq чтобы питон там что-то набрасывал в качестве пруфа?
Нотации — они в Vernacular, а не в Ltac, ЕМНИП. Основное преимущество, что в нём есть backtracking a la Prolog, и он знает всё про термы Gallina, в т.ч. умеет их красиво матчить. Некоторые требовательные к производительности тактики на Ocaml там написаны. В теории можно и питон звать, наверно.
А этот Ltac знает Gallina на уровне некоего AST, или он в своем составе содержит парсер синтаксиса этой Gallina и потом текстушню какую-то набрасывает для пруфанья, которая прогоняется потом через парсер для Gallina в самом Gallina-интерпретаторе и там как-то верифицируется?
P.S. И это делается без парсера, ибо coqtop умеет в holes. Т.е., грубо говоря, компилятор посреди компиляции останавливается и передаёт тактике управление, чтобы она там что-то догенерила. Это вам не анскилльные макросы.
Я ведь тогда не могу в Coq доказать что Coq(Coq(x)) проверяет x и считает этот пруф верным или не верным тогда же, когда, когда это делает Coq(Coq(Coq(x))), даже не смогу это объявить как аксиому(если это недоказуемо из-за какой-то там неполноты), да? И что в этом хорошего?
И вообще, взять например идею с partial evaluation, futamura projection. Говоря простым языком, можно рассматривать Тьюринг-полные языки как некие математически формализуемые питули, и можно сделать декларативное описание одного языка lang1, и декларативное описание другого языка lang2, и придумать функцию gen_transl(dst, src, target) т.е. gen_transl(lang1, lang2, lang1) сгенерит код на языке lang1 который транслирует (или компилирует) язык lang2 в lang1, и все это доказать. Вот https://habr.com/ru/post/47418/ там про это немного побольше написано. Так вот, можно таким вот образом расширять возможности некоторого языка, добавляя в него новые фичи. И если допустим язык gallina формализуем и формализован в gallina, можно взять какой-нибудь другой язык для теорем-прувинга и сделать его транслятор в gallina, и наоборот.
Конечно же нужен язык с гомоикнностью. Нужно сделать на самом языке систему символьных вычислений (ССВ) над его же кодом/AST и используя эту ССВ иметь возможность например выводить определенные свойства реализации (для проведения формальной верификации, доказательства корректности, как например с использованием Frama-C с применением SMT-решателей, Coq, HOL и всякого такого), использовать эту ССВ для целей вроде суперкомпиляции/супероптимизации. Или чтобы циклы например анроллить, типа вот мы задаем каким-то там макаром, что вот тут у нас цикл, и говорим нашей ССВ что вот наанроль его вот таким образом, и потом будет там наанроленный цикл. Или реализовывать свои domain-specific оптимизации для каких-нибудь бигинтов. Или эту же ССВ можно попросить, чтобы например она трансформировала код некой функции таким образом, чтобы она вместо int принимала long long int, чтобы это было еще в IDE интегрировано нормально, и чтобы такую кодогенерацию при желании даже в рантайме можно было бы делать, если с собой в рантайм тащить еще JIT с VM (т.е. тащить какую-то жирную хрень типа JVM) и AST, удобный для трансформации. Можно сделать что-то вроде тех же Java оптимизаций в рантайме, рантайм-профилирование и трансформация кода в процессе...
Или даже profile-guided optimisation (PGO) потом сделать на основе собранной статистики, т.е. вот типа набрали мы статистики при выполнении кода в VM и потом использовали ее чтобы полностью четко скомпилировать в бинарник, чтоб без VM все выполнялось. Чтобы можно было бы вводить свои правила приведения типов, и на основе этого ССВ могла бы выводить тип. Или чтоб можно было сделать язык с нестрогой типизацией поверх существующего AST и чтоб в рантайме при каких-нибудь тестовых прогонах производился мониторинг того, что с какими типами вызывается (т.е. к каким фактически типам там приводится все в динамике) и потом чтобы на основе этого можно было бы расставить эти самые типы в реальном коде. Т.е. если у нас будет функция без указания типа, и эта функция в одном месте вызывается допустим с типом int, а в другом с типом float, то можно сделать две специализированные под этот тип реализации, которые бы вызывались конкретно в тех местах, где собственно и происходит вызов той функции с таким-то там типом.
Нет. Это одна моя старая идея метаязыка для конструирования языков, который будет сам на себе написан, и чтоб всё через частичные вычисления, проекции Футамуры и формальные доказательства там работало, и чтобы это был один единый язык с Тьюринг-полнотой, самомодифицирующийся в процессе исполнения (система переписывающих правил чтоб, грубо говоря запуск языка это самопереписывание графа, полученного из AST с чтением из STDIN выплевыванием чего-то из STDOUT). И на этой алгебре самопереписывания уже б вводились всякие теории типов.
"<...> И на этой алгебре самопереписывания уже б вводились всякие теории типов" -- сказал j123123, докуривая косяк, и начал писать код на сишке под микроконтроллеры.
Раз у Gallina нет тьюринг-полноты и в нем нельзя написать Gallina-интерпретатор, в рамках Gallina нельзя что-то доказывать о том, как что-либо делается самой Gallina для доказывания чего-либо, верно? И нельзя делать эти проекции Футамуры, о которых я выше написал.
На сишных макросах какими-то костылями можно запилить некую сраную поеботу, которая выполняет один шаг брейнфак интерпретатора, но зацикленно вызывать бесконечное количество раз ее не выйдет.
>Now this example is limited to 10 repeats, because of limitations of the counter. Just like a repeat counter in a computer would be limited by the finite memory. Multiple repeat counters could be combined together to workaround this limitation, just like in a computer. Furthermore, we could define a FOREVER macro:
>This will try to output ? forever, but will eventually stop because there are no more scans being applied. Now the question is, if we gave it an infinite number of scans would this algorithm complete? This is known as the halting problem, and Turing completeness is necessary to prove the undecidability of the halting problem. So as you can see, the preprocessor can act as a Turing complete language, but instead of being limited to the finite memory of a computer it is instead limited by the finite number of scans applied.
> Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.
Ну как бы смотря как ты определяешь"класс программ". Если "тьюринг-полный" язык органичен конечной памятью, доказательство зависания для него можно всегда доказать через https://ru.wikipedia.org/wiki/Нахождение_цикла
Рассмотрим функцию "шаг интерпретатора"
state step(state from)
{
делаем некую питушню в зависимости от state,
и вернем новый state
}
Если state это некая хуита, занимающая конечный кусок в оперативной памяти (нет никаких указателей и выделений памяти) то если бесконечный вызов хуйни в хуйню
state st = {someshit};
while(true)
{
st = step(st);
}
То значение `st' обязательно будет повторяться т.к. количество состояний конечно.
И если такая программа выводит что-то в stdout допустим(но ничего не получает извне), то она сводима к:
Т.е. что тут получается. Результат работы зависающей программы на "тьюринг-полном языке с конечной памятью", которая что-то выводит в stdout и ничего не принимает в stdin (или принимает конечную известно какую строку, тогда такая программа сводима к программе, где эта строка тупо в сам код вшита) может быть описана как две конечные строки - строка начальной хуйни, и строка повторяющейся хуйни. Строка начальной хуйни и/или строка конечной хуйни может естественно быть пустой. А две строки конечной длины всегда можно вывести за конечное число шагов.
> Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке.
Некий условный 1 шаг интерпретатора Gallina однозначно можно написать на Gallina т.к. 1 шаг брейнфака написать там точно можно. А вот "вызывать" интерпретатор бесконечное количество раз в Gallina нельзя, и это может сделать только некая внешняя хрень, которая что-то доказывает в терминах Gallina. Как-то так
Как было на самом деле: протоцепепе - ЛИСП 50-80 гг. C++ 80-90 гг. Haskell - новая версия цепепе. 90-00 гг. С точки зрения лиспопетушка сначала был Хаскель, в следующей версии он деградировал до цепепе, а в лиспопетушином будущем цепепе деградирует до лиспа.
А я все ломал голову, как человек может так ненавидеть будущее, так привязаться к прошлому, что пишет на лиспе? Но для лиспопетушка-контрамота лисп - это и есть будущее. А дальше ВВ2, индустриальная контрреволюция, религиозные войны, рабовладельческий строй, отрастание хвостов и подъем на деревья. Скай из зе лимит!
На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом, и всякие CSшни в современном мире без него пилить никому не охота.
> Нет никакого смысла доказывать, что он правильно работает в общем случае
Более того, с его помощью легко запилить что-то неправильное. Ключевые слова Qed. и Defined. потом всё перепроверяют.
Особенный багор, когда ты ltac'ом запилил огромный fixpoint, а он оказался не структурным, т.к. auto где-то подхватило рекуррентный вызов ))) Приходится во избежание этого гипотезы чистить вилкой.
Попытки были (coqhammer, gamepad), насколько успешные не знаю, мне они не помогли. +Я знаю, что сейчас несколько исследовательских групп что-то новое ковыряет.
Вообще, на мой взгляд, самое трудное — это правильные определения. Если в них есть баг или они недостаточно специфичны, то нейросеть просто в какой-то момент встанет или натворит непонятной херни. И потом фиг поймёшь, то ли искуственный идиот что-то напутал, то ли твои определения говно. Ручное доказательство это конечно долго, но зато когда приходишь к какой-то неразрешимой херне, понимаешь, что к чему. Поэтому в данном случае я даже тактику induction не использовал, чтобы она какой-нибудь ненужной херни в гипотезу индукции не подхватила, и запилил индукцию вручную.
Гроссмейстер вошел в зал. Он чувствовал себя бодрым и твердо знал, что первый ход e2 — e4 не грозит ему никакими осложнениями. Остальные ходы, правда, рисовались в совершенном уже тумане, но это нисколько не смущало великого комбинатора.
Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.
Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...
З.Ы. Ня, привет.
Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.
т.е. есть генератор стратегий, ему дают теорему, он выплевывает стратегию gen_strateg(theorem) -> strategy
и есть бесконечно генерирующая теоремы херня, допустим gen_theorem(0) - одна теорема, gen_theorem(1) - другая, и так далее.
А потом надо доказать что Так делают?
Вопрос я, конечно, не понял, но ответ на него скорее всего – нет. Дело в том, что стратегий в Coq нет, есть тактики, и они пишутся на совершенно другом метаязыке (Ltac), нежели теоремы (Gallina). (В Lean не так, кстати. Там по слухам гомоиконность) Поэтому написать теорему про тактику в Coq – это как написать функцию, принимающую как аргумент макрос, в C.
У `стратегии' тип это список правил, по которым некая питушня что-то набрасывает в качестве пруфа теоремы, пытаясь это доказать. Ну ок, пусть будет `тактики', а не `стратегии'. Почему б не доказывать, что такие-то тактики, генерируемые на основе конкретных теорем, всегда успешно доказывают теоремы, сгенеренные таким-то способом? Т.е. доказать что генератор тактик всегда для такого семейства теорем, генерируемых таким способом, генерит такие тактики, которые всегда доказывают соотв. теорему
А почему не сделать это одним языком? Чтобы можно было доказывать доказуемость некоего множества теорем такими-то генеренными из теорем тактиками.
Нянужно! Gallina имеет крайне строгую семантику, поскольку она является доверенной по принципу де Бройля. Поэтому в ней не может быть никаких свистелок и перделок, и всё крайне ограничено и консервативно. А Ltac – не доверенный язык, в нём можно сколько угодно фич пилить и ломать семантику как хочешь. Поэтому его используют для автоматизации, т.к. удобно.
Ну так почему б не написать транспилер из Ltac в Gallina? В самой Gallina сделать тьюринг-полноту с гомоиконами, и пусть само с собой там метушится, доказывая доказуемость.
Принципиально нявозможно. Ltac – Тьюринг полный, Gallina – нят.
Зачем? Зачем? Я могу описать функцию, принимающую стейт брейнфака возвращающую новый стейт брейнфака плюс номер шага, и через Ltac я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота. Ради чего это?
Во-первых, Ltac – логический язык, типа пролога. Формально описывать на Gallina шаг Ltac, и затем применять его с помощью Ltac – это как бутылку кваса провести через весь пищеварительный тракт наверх ко рту, чтобы вылить всё её содержимое в дыхательное горло.
> я могу сделать тактику чтобы bf_step(....bf_step(bf_step(bf_step( bf_initial_state))).....) и будет тоже тьюринг-полнота
Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Чтобы доказывать применимость таких-то стратегий (стратегий, построенных по определенному шаблону) к доказыванию таких-то теорем, построенных по определенному шаблону. Сделать еще какую-то алгебру стратегий, что такие-то стратегии можно упростить, сведя их к таким-то, а вот такие стратегии это частные случаи таких стратегий. Более высокий уровень абасракции короче.
> Ня будет. Ты сейчас предлагаешь бесконечный цикл заанроллить.
Почему не будет? Так мы пробуем доказать небесконечность цикла, и раз мы так можем делать, это и есть тьюринг-полнота, мы интерпретируем брейнфак. Какая разница, зависнет ли у меня Ltac генерящий питушню для Gallina, или Gallina само себе питушню генерить будет и зависнет?
Огромная. [1] [2]
[1] https://govnokod.ru/26981#comment579147
[2] https://govnokod.ru/27333#comment620156
Поднимаю говно-Хирш
В переводе на петушиный: у меня есть функция F(n : nat), возвращающая термы в универсуме U + 1.
> Есть генератор тактик, тактика1 доказывает теорему1, тактика2 доказывает теорему2 и так далее.
В переводе на петушиный: у меня есть функция G от nat, которая возвращает терм типа F(n) в универсуме U.
> И надо доказать, что все такие генеретные тактики доказывают все такие генеренные теоремы.
В переводе на петушиный: надо найти определение G.
> Почему это не в рамках единого языка?
Просто переформулировав пробему как показано выше, ты и сделаешь это в рамках одного языка.
А тактики – это макроязык такой.
Переформулировать-то можно, это понятно. Но так не выйдет доказать что-то относительно неких свойств стратегий, применимости определенных стратегий к доказыванию определенных типов теорем и так далее. Окажись стратегий частью самого языка для описания теорем, это можно было бы делать.
В этом вроде и идея ltac. Нет никакого смысла доказывать, что он правильно работает в общем случае или для каких-то классов теорем. Достаточно просто проверять сгенерённые им пруфы для конкретных теорем которые тебе и нужно доказать.
А технически и питон и даже пхп сойдут, конечно.
Причина: ты что, пёс, я Computer Scientist.
Ну а на деле: люди бы ебанулись на LISP паттерн-матчинг типов пилить. Да в нём и нету нормального паттерн-матчинга.
Тогда еще больше причин делать всю петушню в рамках одного языка, а не разграничивать на две хрени, которые там еще как-то перепихиваются в процессе.
Я ведь тогда не могу в Coq доказать что Coq(Coq(x)) проверяет x и считает этот пруф верным или не верным тогда же, когда, когда это делает Coq(Coq(Coq(x))), даже не смогу это объявить как аксиому(если это недоказуемо из-за какой-то там неполноты), да? И что в этом хорошего?
Это копипаста, которую я хуй знает когда написал.
Это вореции?
Нет. Это одна моя старая идея метаязыка для конструирования языков, который будет сам на себе написан, и чтоб всё через частичные вычисления, проекции Футамуры и формальные доказательства там работало, и чтобы это был один единый язык с Тьюринг-полнотой, самомодифицирующийся в процессе исполнения (система переписывающих правил чтоб, грубо говоря запуск языка это самопереписывание графа, полученного из AST с чтением из STDIN выплевыванием чего-то из STDOUT). И на этой алгебре самопереписывания уже б вводились всякие теории типов.
Если б мне кто-то профинансировал запиливания хрени, которую я расписал, я б ее очень даже охотно писал.
Раз у Gallina нет тьюринг-полноты и в нем нельзя написать Gallina-интерпретатор, в рамках Gallina нельзя что-то доказывать о том, как что-либо делается самой Gallina для доказывания чего-либо, верно? И нельзя делать эти проекции Футамуры, о которых я выше написал.
Т.к. Gallina не Тьюринг-полна, в теории может и можно написать её интерпретатор на не-Тьюринг полном языке. Напиши, проверишь.
На сишных макросах? Они как раз не тьюринг полны.
https://github.com/orangeduck/CPP_COMPLETE
https://github.com/pfultz2/Cloak/wiki/Is-the-C-preprocessor-Turing-complete%3F
>Now this example is limited to 10 repeats, because of limitations of the counter. Just like a repeat counter in a computer would be limited by the finite memory. Multiple repeat counters could be combined together to workaround this limitation, just like in a computer. Furthermore, we could define a FOREVER macro:
>This will try to output ? forever, but will eventually stop because there are no more scans being applied. Now the question is, if we gave it an infinite number of scans would this algorithm complete? This is known as the halting problem, and Turing completeness is necessary to prove the undecidability of the halting problem. So as you can see, the preprocessor can act as a Turing complete language, but instead of being limited to the finite memory of a computer it is instead limited by the finite number of scans applied.
Т.е. это явно более узкий класс программ чем в типичном "тьюринг-полном" языке, который ограничен только памятью.
Ну как бы смотря как ты определяешь"класс программ". Если "тьюринг-полный" язык органичен конечной памятью, доказательство зависания для него можно всегда доказать через https://ru.wikipedia.org/wiki/Нахождение_цикла
Рассмотрим функцию "шаг интерпретатора"
Если state это некая хуита, занимающая конечный кусок в оперативной памяти (нет никаких указателей и выделений памяти) то если бесконечный вызов хуйни в хуйню
То значение `st' обязательно будет повторяться т.к. количество состояний конечно.
И если такая программа выводит что-то в stdout допустим(но ничего не получает извне), то она сводима к:
или принимает бесконечную периодическую строку, такую строку тоже можно в код вшить.
Некий условный 1 шаг интерпретатора Gallina однозначно можно написать на Gallina т.к. 1 шаг брейнфака написать там точно можно. А вот "вызывать" интерпретатор бесконечное количество раз в Gallina нельзя, и это может сделать только некая внешняя хрень, которая что-то доказывает в терминах Gallina. Как-то так
https://archive.jlongster.com/Lisp--It-s-Not-About-Macros,-It-s-About-Read
А я все ломал голову, как человек может так ненавидеть будущее, так привязаться к прошлому, что пишет на лиспе? Но для лиспопетушка-контрамота лисп - это и есть будущее. А дальше ВВ2, индустриальная контрреволюция, религиозные войны, рабовладельческий строй, отрастание хвостов и подъем на деревья. Скай из зе лимит!
На самом деле в Lisp и Scheme всё очень печально с pattern-matching'ом, и всякие CSшни в современном мире без него пилить никому не охота.
В чем именно заключается печальность? Что мешает сделать DSL для pattern-matching'а?
Его там нет. (Ну может в современных диалектах появился)
> Что мешает сделать DSL для pattern-matching'а?
Так сделали, само собой. Но когда я открываю доки по pcase, я плачу, настолько он уродливый.
https://docs.racket-lang.org/reference/match.html такой паттерн матчинг норм? Покажи реальный пример хорошего паттерн-матчинга в каком-то язычке.
Более того, с его помощью легко запилить что-то неправильное. Ключевые слова Qed. и Defined. потом всё перепроверяют.
Особенный багор, когда ты ltac'ом запилил огромный fixpoint, а он оказался не структурным, т.к. auto где-то подхватило рекуррентный вызов ))) Приходится во избежание этого гипотезы чистить вилкой.