LINUX.ORG.RU

refinement type, формальная верификация в нефункцональных языках?

 , refinement type, , ,


3

3

Я вот что подумал - почему вынесенные в заголовок штуки в основном применяются в ФП с жирным рантаймом GC? Это ж вполне можно и в более нормальных языках заюзать.

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

  uint32_t a[100];

  for (size_t i = 0; i < 100; i++)
  {
    if ( scanf("%" SCNu32 "\n", &a[i]) != 1)
    {
      exit(-1);
    }
  }

Вот после этого for цикла (если не произошло exit (-1)) в массиве a[100] образовались какие-то там данные, нам про них ничего в точности неизвестно, там пользователь что попало мог ввести.

Скажем, если мы после этого сделаем такое:

  for (size_t i = 0; i < 100; i++)
  {
    printf("%" PRIu32 "\n", 100500 / a[i]);
  }
То у нас нет гарантии что этот код завершится корректно т.к. в этом a[i] может быть 0 и будет SIGFPE.

А если например перед этим сделать нечто такое

  for (size_t i = 0; i < 100; i++)
  {
    if(a[i] == 0)
    {
      a[i] = 1;
    }
  }
То тогда норм. Вот я хочу, чтобы код в котором может возникнуть ошибка SIGFPE из-за поступления внешних непроверенных данных — вообще не компилировался.

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

Ну и это еще можно использовать для оптимизации, скажем если мы отсортировали некий массив, то потом если мы пытаемся его отсортировать второй раз подряд, то во-первых можно вывести предупреждение от компилятора «этот массив и так сортирован, нечего его сортировать» а во-вторых можно просто вызов сортировки выкинуть т.к. он ничего не делает. Ну и кроме того, есть алгоритмы которым обязательно сортированные данные нужны, например это алгоритм двоичного поиска. Можно на каком-то языке описать, что алгоритм двоичного поиска, если ему на вход подать сортированный массив, он там сможет найти некий элемент если он там точно есть и не найти если его нет. А если ему несортированный массив подать (т.е. для которого нет свойства что a[n] <= a[n+1] для всех n от 0 до размермассива) то тогда это уже неверно, т.е. должна быть ошибка компиляции, если мы не проверенные на сортированность данные пускаем на вход к двоичному поиску

Вообще, есть такой GNU экстеншен __builtin_unreachable() и им можно например такую ерунду вытворять https://godbolt.org/z/dN6ozS

#define ALWAYS_FALSE(a) if(a) __builtin_unreachable()
#define ALWAYS_TRUE(a) ALWAYS_FALSE(!(a))

unsigned div_eq(unsigned a, unsigned b)
{
  ALWAYS_TRUE(a == b);
  ALWAYS_TRUE(a != 0);
  return a/b;
}

unsigned div(unsigned a, unsigned b)
{
  return a/b;
}

Ну и тут вариант div_eq оптимизируется до return 1; (шланг неосиливает) - но это все костыли. И язык аннотаций из Frama-C это тоже костыли - из них такую оптимзацию не сделать, это внешний костыль для проверки контрактов.

Почему нет нормального компилируемого в натив языка без жирного рантайма с GC, чтоб там можно было вот так специфицировать поведение функций, допустимые входные параметры, кванторы-шманторы там, чтоб это все проверялось и оптимизировалось на основе спецификации-контрактов? И чтоб с суперкомпиляцией!

★★★★★

Последнее исправление: SZT (всего исправлений: 2)

ИМХО

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

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

anonymous
()

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

Не удивлюсь, если какой-нибудь подобный академический язык есть.

xaizek ★★★★★
()
Последнее исправление: xaizek (всего исправлений: 1)
Ответ на: комментарий от xaizek

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

Почему любой? Надо просто ограничить. Ну например, если у нас есть глобальный массив и с ним можно взаимодействовать только функциями sort(), bsearch(), set() - то вот если мы массив заполним функцией set() то функция bsearch() не может быть вызвана т.к. мы не уверены в сортированности. А если мы сделали sort() - bsearch() вызывать можно.

SZT ★★★★★
() автор топика
Ответ на: комментарий от x3al

Это конечно интересно, но не то. Мне нужна условная сишка с формальной верификацией, суперкомпиляцией, refinement type и контрактами с кванторами, а не некий функциональный язык который непойми как в сишку оттранслируется (не факт что оптимально, не факт что компилятор сможет это соптимизировать вменяемо в сравнении с тем если б я тупо на Си все это написал, и так далее).

SZT ★★★★★
() автор топика
Последнее исправление: SZT (всего исправлений: 2)
Ответ на: комментарий от SZT

Я потом добавил слово «практически». Каждое такое расширение надо включать в язык «безопасным» образом, так что каждый эффект был бы учтён. Наверное, стоило написать «неучтённый эффект», а не «возможный», я это имел в виду.

xaizek ★★★★★
()
Последнее исправление: xaizek (всего исправлений: 1)
Ответ на: комментарий от anonymous

Похоже в нужном направлении, в смысле императивности, но он на JVM. При этом даже простые функции уже довольно муторно писать, судя по примерам. Но оно может того стоить.

xaizek ★★★★★
()
Ответ на: комментарий от x3al

Ну и vale это что-то типа ассемблера с контрактами, писать отдельно под x86, x86-64, ARM - не есть хорошо.

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

Эмм. Функциональный язык, транслирующийся в читабельный С с гарантией, что каждая функция завершается и делает то, что ты хочешь, может быть заметно проще на практике, чем реальный C.

Софт, юзающий malloc свободно, невозможно верифицировать вообще.

x3al ★★★★★
()
Ответ на: комментарий от SZT

Хм. Из всей верифицируемой императивщины гугл знает разве что spark pro, но я без понятия, насколько нормально писать софт на подмножестве ada с закрытым компилятором в 2к20 году.

x3al ★★★★★
()

Мне нужна условная сишка

Вот тебе язык от Microsoft: https://github.com/microsoft/checkedc

The goal of the project is to improve systems programming by making fundamental improvements to C

Есть под Linux, потому что Microsoft любит Linux…

fsb4000 ★★★★★
()
Последнее исправление: fsb4000 (всего исправлений: 2)
Ответ на: комментарий от x3al

Софт, юзающий malloc свободно, невозможно верифицировать вообще.

Не мешай ему - он хочет верифицировать UB.

anonymous
()
Ответ на: комментарий от anonymous

он хочет верифицировать UB.

Надо отсутствие любых UB верифицировать. Чтоб не было проблемы разыменования NULL после malloc, можно сделать чтоб программа при старте выделяла себе нужное разрешенное количество оперативки (нельзя выделить при старте - программа не запустится), и потом там делать аллокатор и доказывать, что программа никогда за лимиты не вылезет т.е. невозможность ситуации что malloc где-то вернет NULL

SZT ★★★★★
() автор топика
Ответ на: комментарий от x3al

Софт, юзающий malloc свободно, невозможно верифицировать вообще.

Можно верифицировать, если malloc() заменить на xmalloc()

void * xmalloc (size_t size)
{
  void *new_mem = (void *) malloc (size);
  if (new_mem == NULL)    
  {
    exit (-1);
  }
  return new_mem;
}
т.е программа или упадет от нехватки памяти, или всё будет норм.

Такой гарантии тоже может быть достаточно для каких-то применений

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

SZT ★★★★★
() автор топика
Последнее исправление: SZT (всего исправлений: 1)
Ответ на: комментарий от SZT

Чтоб не было проблемы разыменования NULL

Может, надо сперва надо решить проблему с (отсутствующей) системой типов у си? И не превратится ли си после решения этой проблемы в какой-нибудь вполне императивный язык программирования ((o)ca)ml?

anonymous
()
Ответ на: комментарий от anonymous

И не превратится ли си после решения этой проблемы в какой-нибудь вполне императивный язык программирования ((o)ca)ml?

Ну и пусть превращается, у меня нет непереносимости ML языков. Главное чтоб там GC и прочего рантайма не было

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

Ну и пусть превращается, у меня нет непереносимости ML языков. Главное чтоб там GC и прочего рантайма не было

И чем тогда тебе кремль не угодил?

anonymous
()
Ответ на: комментарий от x3al

Софт, юзающий malloc свободно, невозможно верифицировать вообще.

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

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

В этом как бы весь смысл fstar:

For instance, in ML (canRead «foo.txt») is inferred to have type bool. However, in F*, we infer (canRead «foo.txt» : Tot bool). This indicates that canRead «foo.txt» is a pure total expression, which always evaluates to a boolean. For that matter, any expression that is inferred to have type-and-effect Tot t, is guaranteed (provided the computer has enough resources) to evaluate to a t-typed result, without entering an infinite loop; reading or writing the program's state; throwing exceptions; performing input or output; or, having any other effect whatsoever.

On the other hand, an expression like (read «foo.txt») is inferred to have type-and-effect ML string, meaning that this term may have arbitrary effects (it may loop, do IO, throw exceptions, mutate the heap, etc.), but if it returns, it always returns a string. The effect name ML is chosen to represent the default, implicit effect in all ML programs.

Tot and ML are just two of the possible effects. Some others include:

Dv, the effect of a computation that may diverge;

    ST, the effect of a computation that may diverge, read, write or allocate new references in the heap;
Exn, the effect of a computation that may diverge or raise an exception.

рекурсивных вызовов функций

Tot гарантирует, что функция завершится. Этого достаточно для безопасного использования рекурсии?

x3al ★★★★★
()
Ответ на: комментарий от SZT

Можно верифицировать, если malloc() заменить на xmalloc()

Только это не спасает от утечек памяти. И проверить нетривиальный софт на C на утечки статичным анализом в общем случае нереально.

https://en.wikipedia.org/wiki/Shape_analysis_(program_analysis)

x3al ★★★★★
()
Ответ на: комментарий от anonymous

И чем тогда тебе кремль не угодил?

Например тем, что это транслятор в Си. И про суперкомпиляцию там я что-то не нашел ничего.

Я хочу чтоб например условный код

unsigned div_eq(unsigned a, unsigned b)
{
  ALWAYS_TRUE(a == b);
  ALWAYS_TRUE(b != 0);
  return a/b;
}
трансформировался какими-то умными алгоритмами в
unsigned div_eq(unsigned a, unsigned b)
{
  return 1;
}

Я хочу чтоб если где-то вызывается обычная функция деления

unsigned div(unsigned a, unsigned b)
{
  return a/b;
}

и в том месте где она вызывается, доказано на этапе компиляции что a == b и b != 0 то тогда деления не происходит, просто возвращается 1. И если там доказано что b > a и b != 0 то тогда тоже деления не происходит, возвращается 0.

Да и можно ж сделать что сам компилятор можно было б на этапе компиляции допиливать своими доказанными специализированными domain-specific оптимизациями, например вот работаете вы где-то с bigint-ами, и чтоб можно было б делать оптимизации вида (a + b) * (a^2 - ab + b^2) -> a^3 + b^3 ну и через бином ньютона чтоб на произвольные степени обобщить. Нужна какая-то полноценная система символьных вычислений на уровне AST языка с возможностью доказывать корректность трансформаций (сохранения семантик). Я не вижу чтоб в KreMLin такие фичи были

SZT ★★★★★
() автор топика
Ответ на: комментарий от x3al

Tot гарантирует, что функция завершится. Этого достаточно для безопасного использования рекурсии?

Речь о том, чтоб гарантировать что не будет падения от переполнения стека из-за рекурсии. Для этого необязательно делать бесконечную рекурсию. Если я каким-то образом задам лимит стека вызовов (с адресами возврата и локальными переменными), я могу доказать, что этот лимит не будет превышен?

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

Я хочу …

Как только решишь NP-полную задачу доказательства теорем с использованием разумного количества ресурсов, в том числе временых.

anonymous
()
Ответ на: комментарий от SZT

И если там доказано что b > a и b != 0 то тогда тоже деления не происходит, возвращается 0.

Подожди. Ты хочешь чтобы это доказывал компилятор за тебя и автоматически оптимизировал исходя из этого?

x3al ★★★★★
()
Ответ на: комментарий от SZT

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

x3al ★★★★★
()

Прямо как ты хочешь нету, но для верификации есть Frama-C.

А вообще можно просто eDSL на хацкелле верифицировать и в C компилить. Я видел типизированный ассемблер для 6502, сделанный таким образом.

hateyoufeel ★★★★★
()
Последнее исправление: hateyoufeel (всего исправлений: 1)

Кто будет этим заниматься? ML убило весь компуктер сайнс, никому не интересно пердолиться с верификацией и суперкомпиляцией, когда можно клепать нейросетки за 300к/сек.

buddhist ★★★★★
()
Ответ на: комментарий от buddhist

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

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

доказано на этапе компиляции

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

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

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

olelookoe ★★★
()
Ответ на: комментарий от olelookoe

допустим

  1. каждый узел предшествуется предусловием.

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

проблема все-этого полная пересборка этих всех контрактных проверок при изменении подграфов вызовов - т.е. вопрос цены :(

qulinxao3
()
Ответ на: комментарий от x3al

Так в Ada 2012 добавили некоторые шткуки из Spark. Но малую часть, конечно. Другое дело, что Аде не помогает её система типов и инварианты в плане оптимизаций и она всё равно медленная с пухленьким рантаймом.

anonymous
()

Суперкомпиляция сама по себе сложная. И разрабатывалась на сколько я понимаю именно для функциональных языков (имею ввиду РЕФАЛ, конечно). Попытка присобачить её к яве(?) провалилась, при этом это дело финансировалось вроде бы саном. Т.е. сложность этого дела мягко говоря не маленькая. Вроде как суперкомпилятор построен для хаскеля, но что там я лично не знаю.

Тут тонкий момент в том что система типов в функциональных языках, она не с потолка. Она из всяких там лямбда-кубов и прочих там штук. По поводу которых довольно много известно хорошего (типа вот так точно можно, а вот так точно нельзя). Для произвольной системы типов произвольного языка этих знаний нет (ну как нет.. известно много, но это либо слишком сложно, как в случай с ООП, либо довольно примитивно, как в си, например), поэтому, как я понимаю, и хорошее доказательство на этапе компиляции построить сложно. Есть системы верификации типа валгринда или рекламируемого тут часто для си++ чекера какого-то.

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

В хаскеле есть возможность писать аннотации (не помню как называется). Но это получается что то вроде отдельного расширения системы типов.

Для объектно ориентированных языков там вообще на сколько мне известно кадавр по сложности системы типов, не продерёшся.

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

AndreyKl ★★★★★
()
Последнее исправление: AndreyKl (всего исправлений: 2)

http://www.ats-lang.org/ внезапно, гугль рассказал про ещё один низкоуровневый язык с зависимыми типами. Но подозреваю, что в мире примерно 0 его юзеров.

x3al ★★★★★
()
Ответ на: комментарий от x3al

http://www.ats-lang.org/

Слишком сложно писать. В коде больше логики над типами, чем бизнес-логики. Примерно 2/3 кода - это описание типа, аксиомы-леммы-теоремы и тп. А половина из оставшей третьи - это борьба с тайпчекером. При генерации си-кода слишком много мусорных выделеней и удалений памяти под каждый чих - нет даже минимальной оптимизации на уровне языка.

anonymous
()
Ответ на: комментарий от anonymous

Примерно 2/3 кода - это описание типа, аксиомы-леммы-теоремы и тп

Звучит нормально для языка с зависимыми типами.

x3al ★★★★★
()
Ответ на: комментарий от x3al

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

anonymous
()
Ответ на: комментарий от AndreyKl

Суперкомпиляция сама по себе сложная. И разрабатывалась на сколько я понимаю именно для функциональных языков (имею ввиду РЕФАЛ, конечно). Попытка присобачить её к яве(?) провалилась, при этом это дело финансировалось вроде бы саном. Т.е. сложность этого дела мягко говоря не маленькая. Вроде как суперкомпилятор построен для хаскеля, но что там я лично не знаю.

Вот есть статья «Особенности применения метода частичных вычислений к специализации программ на объектно-ориентированных языках»: https://keldysh.ru/papers/2008/prep12/prep2008_12.html

Про специализаторы для языка Си там тоже что-то упоминается.

Еще в начале 90х готов Ларс Оле Андерсен (Lars Ole Andersen) в университете Копенгагена в Дании разработал [Ande91,Ande93,Ande94] специализатор С-MIX для языка C.

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

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

Не, частичные вычисления — это немного про другое. Refinement type — это когда ты объявляешь, что функция, принимающая векторы длиной M и N вернёт вектор длиной M + N, где M и N задаются в рантайме, а компилятор тебе в compile time проверяет доказательство, что твоя функция именно так себя ведёт. Это нифига не тривиально, поскольку задаётся в рантайме.

А оптимизация через выкидывание лишнего кода — это то, чем gcc/llvm постоянно занимаются. Она делает только то, что можно сравнительно просто сделать в compile time.

x3al ★★★★★
()
Ответ на: комментарий от x3al

Refinement type — это когда ты объявляешь, что функция, принимающая векторы длиной M и N вернёт вектор длиной M + N, где M и N задаются в рантайме, а компилятор тебе в compile time проверяет доказательство, что твоя функция именно так себя ведёт.

Ну вообще-то я б не сказал. Вот допустим есть у нас функция concat(a,b), принимающая векторы a, b и возвращающая c. Если мы потом где-то в коде программы сравниваем veclen(a) <= veclen(c) то компилятор может эту проверку выкинуть, заменив на true т.к. из свойств функции concat и истории жизни переменных a, c следует, что сравнение veclen(a) <= veclen(c) обязательно вернет true. Это и будут частичные вычисления.

По-моему тут есть явная связь и есть смысл это совместить

SZT ★★★★★
() автор топика
Последнее исправление: SZT (всего исправлений: 1)
Ответ на: комментарий от x3al

А оптимизация через выкидывание лишнего кода — это то, чем gcc/llvm постоянно занимаются. Она делает только то, что можно сравнительно просто сделать в compile time.

Да, компиляторы это делают весьма посредственно: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=92233

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

из свойств функции concat

которые ты руками докажешь

и истории жизни переменных

Этого нет в compile time, сейчас речь же не идёт о JIT?

x3al ★★★★★
()
Ответ на: комментарий от x3al

которые ты руками докажешь

Ну допустим руками. А потом на основе руками доказанного свойства можно сделать оптимизацию.

Этого нет в compile time, сейчас речь же не идёт о JIT?

Нет, насчет JIT - неJIT я не конкретизировал. Можно с JIT, можно и без JIT.

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

> vec a = read(/dev/urandom, random_in_range(0, 100));
> vec b = read(/dev/urandom, random_in_range(0, 100));
// прочитали случайное количество (от 0 до 100) байт из /dev/urandom и всунули в вектор

> vec c = concat(a, b);
// Вот тут для типа vec c есть особые свойства
// Которые можно описать таким образом:
// ALWAYS_TRUE( (veclen(c) <= veclen(a)) && (veclen(c) <= veclen(b)) )

// Если у нас интерпретатор или некая ерунда с жирным рантаймом
// типа JVM с возможностью динамически подгружать непойми откуда непойми какой байткод,
// и уметь с этим подгруженным в рантайме байткодом делать какие-то хитрые оптимизации
// этот constraint можно хранить в переменной и в процессе интерпретации или JIT-а его учитывать

// Если же у нас нормальный компилятор и если и все можно разрулить на этапе компиляции
// никакой необходимости таскать с собой этот constraint нет

SZT ★★★★★
() автор топика
Ответ на: комментарий от SZT

Если мы потом где-то в коде программы сравниваем veclen(a) <= veclen(c) то компилятор может эту проверку выкинуть, заменив на true

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

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

anonymous
()
Ответ на: комментарий от anonymous

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

В примитивных - да. Хотя во всех да.

Думаю, в общем случае такое невозможно.

Возможно.

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

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

size(concat(a, b)) == size(a) + size(b) - это аксиома, свойство операции. Во всякой запартной херне все эти аксиомы захардкодены для мусорных списков, а далее уже фокусы над ними.

Но тебе не обязательно этим заниматься. Ты можешь попросту обвесить аксиомами все свои базовые операции.

Далее из этой аксиомы выводится всё остальное. Но ничего даже ненужно выводить. Ты можешь напрямую использовать эту информацию при реализации eq.

Если a + b == с, то a <= c. Очевидно, что арифметика беззнаковая.

В базовой реализации просто можно хардкодить правила на базе простых связей. c <- concat(a, b). И далее если у одного аргумента источник - конкат, а у второго ребёнок этого concat, то при сравнении их - ребёнок будет всегда меньше, либо равен.

Очевидно, что далее всё это можно обобщить. Но для начала хватит и этого.

pacer_gracyn
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.