Снова о статической типизации

Кстати, было бы весьма интересно, если бы линейные типы официально добавили в спецификацию Си.

Так указатели и есть они самые. В контексте того, что «использование» это free и realloc. Проблема в том, что проверить во всех случаях нельзя, поэтому у нас есть условно работающий -fanalyse и UB при «нарушении типа».

Четко очертить границу проверяемого и в его рамках действовать – это уже практически полезно.

Линейный тип в рамках автоматических переменных aka переменные на стеке может быть весьма просто и строго формально реализован, а пользы от него будет – вагон.

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

Туда же проблемы с подсчетом ссылок. Чтобы вот эти «transfer none» и «transfer full» из документации перестали быть просто словами без проверки.

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

Это -fanalyzer и так ловит.

Чтобы вот эти «transfer none» и «transfer full» из документации перестали быть просто словами без проверки.

Достаточно добавить __attrubute__ для -fanalyzer. Я удивлён, что есть атрибут malloc, но нет для возможности указать, что внешняя функция вызывает какой-то из деаллокаторов.

https://andreykl.github.io/mapcar/mapcar.html

Там надо зажимать «альт» и стрелкой «вниз» компилируется построчно. Первая строчка компилируется медленно (подгружаются и компилируются файлы, надо подождать). Потом быстро.

Примеры внизу страницы.

Когда дойдёшь до примеров (нажимая альт+вниз), то справа в панельке смотри результат.

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

В общем, гляди.

Круто. Вот только вместо лаконичного

(defun my-mapcar (fn xs &rest lists)
  (cond 
     ((null xs) nil)
     ((null lists) (cons (funcall fn (car xs))
                         (my-mapcar fn (cdr xs))))
     (t (cons (apply fn (car xs) (my-mapcar #'car lists))
              (apply my-mapcar fn (cdr xs) (my-mapcar #'cdr lists))))))

получаем портянку

Fixpoint fs {ts tres} n (f : Tf tres ts) : IList (Tf tres ts) n :=
  match n with
  | O => []
  | S n => f :: fs n f
  end.

Fixpoint reduce
  {n t ts tres}
  (fs : IList (Tf tres (t::ts)) n) (args : IList t n) : IList (Tf tres ts) n :=
  match fs in IList.t _ n return IList.t _ n -> n = n -> _ with
  | [] => fun _ _ => []
  | f :: fs =>
      fun '(a :: args) e =>
        let args := let 'eq_refl := e in args in f a :: reduce fs args
  end args eq_refl.

Open Scope hlist_scope.

Fixpoint reduce_lists {n ts tres} (lists : HList n ts)
  : IList (Tf tres ts) n -> IList tres n :=
  match lists with
  | [] => fun res => res
  | as__t :: as__ts =>
      fun fs =>
        let fs := reduce fs as__t in
        reduce_lists as__ts fs
  end.

Definition mapcar1 {ts n tres} (lists : HList n ts) (f : Tf tres ts)
  : IList tres n :=
  let fs := fs n f in reduce_lists lists fs.

С другой стороны, если это удалось написать, то потом меньше ошибок с этим mapcar.

С третьей, это удалось сделать на Coq, но не, например, на Haskell. Это про то, что не все системы типов одинаково мощны. На Typed Racket вообще можно написать тип:

(All (c a b ...)
   (-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c)))

Хотя на Coq ещё и длину списков проверяет, на Typed Racket нет.

(fn xs &rest lists)

что это за конструкция? ну, fn - функция, xs - это наши списки, а &rest lists?

[в попытках не запутаться в скобочках]

UPD. прошу прощения, запутался, это ведь наши списки опционально, у нас ведь их много..

Хорошее решение, действительно лаконичное.

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

Правда, если воспользоваться расширениями как тут https://blog.poisson.chat/posts/2018-06-06-hlists-dependent-haskell.html (читал эту статейку кажется лет пяток назад), то можно я думаю хаскеле изобразить, но на 100% не уверен. Правда там не очень красиво с синглтонами выходит, но это уже техника, а не теория.

Тут ещё надо сказать я написал что пришло в голову, - создал массив функций и применял по одному аргументу в reduce. Т.е. решение моё не оптимальное. Разница с твоим в том что массив результатов создаётся на лету. Надо попробовать будет, если руки дойдут.

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

что это за конструкция? ну, fn - функция, xs - это наши списки, а &rest lists?

Аргументы. fn - первый (функция), xs - второй (список), lists - остальные (список списков получается).

Аргументы. fn - первый (функция), xs - второй (список), lists - остальные (список списков получается).

Да, разобрался, спасибо.

можно я думаю хаскеле изобразить

Ну без динамических фич, ясное дело. Так то можно мне кажется конечно.

Тут ещё надо сказать я написал что пришло в голову, - создал массив функций и применял по одному аргументу в reduce. Т.е. решение моё не оптимальное. Разница с твоим в том что массив результатов создаётся на лету. Надо попробовать будет, если руки дойдут.

А моё типизацию не проходит…

(my-mapcar #'car lists) пытается применить функцию к списку из разных элементов.

сильная нормализация (т.е. программы которые типизируются зависимыми типами не могут зависнуть)

n = 1
while(some_math(n)) n++;
return n

как будет типизироваться?

Правда, если воспользоваться расширениями как тут https://blog.poisson.chat/posts/2018-06-06-hlists-dependent-haskell.html (читал эту статейку кажется лет пяток назад), то можно я думаю хаскеле изобразить, но на 100% не уверен. Правда там не очень красиво с синглтонами выходит, но это уже техника, а не теория.

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

while в общем случае описать нельзя, поскольку он, очевидно, может не закончиться

while(1) n++;

Fixpoint while(step n : nat) : nat :=
  match step with
  | O => n
  | S step => 
     let step := some_math n step in
     while step (S n)
  end.

А моё типизацию не проходит…

(my-mapcar #'car lists) пытается применить функцию к списку из разных элементов.

не знаю, я общий смысл вроде уловил)

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

да, там видны некоторые сложности с практикой, согласен

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

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

Вообще говоря, самый наверное безгеморойный способ - это написать монадическое окружение по типу вот такого

https://stackoverflow.com/questions/32504352/imperative-loop-in-haskell

https://hackage.haskell.org/package/monad-loops-0.4.3/docs/Control-Monad-Loop...

(я думаю ты знаком).

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

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

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

Кстати, хороший пример от alysnix.

Nat f(Nat k) { 
  if(k == 1) return 1;
  if(k > 100000000000) return 0;
  if(k % 2 == 0) return f(k/2);
  return f(2*n+1);
}

Функция гарантированно завершается. Сможет Coq её скомпилировать?

C n++ то синтаксис, понятно, что в чистых языках без монады никак. Считай, что обычная хвосто-рекурсивная. В предыдущем сообщении корректный пример.

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

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

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

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

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

В смысле? Оно запустит для всех k от 1 до 100000000000 при компиляции?

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

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

В Typed Racket всегда можно завернуть в cast к нужному типу, если проверялка не может доказать корректность, но программист точно уверен (в коде будет добавлена динамическая проверка на случай, если программист всё-таки неправ).

while в общем случае описать нельзя, поскольку он, очевидно, может не закончиться

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

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

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

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

Да. Именно Кок интересуется лишь теоретической завершаемостью. Т.е. он должен доказать что программа [а точнее запускаемая в коке функция] завершиться в принципе. Время завершения его по умолчанию не интересует.

Но если ты такое условие ставишь, ты сам понимаешь что твой код надёжным не является.

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

Это удобно например для трансляции императивных программ [в coq с целью доказательства их корректности]. Императивные программы транслируют в монады (руками или автоматически). Тут важно чтобы всё скомпилировалось, поэтому монады очень удобны. И не важно какое число передавать в run поскольку код запускать никто не будет. А потом доказывают что всё-таки всё завершится когда надо и без ошибок. Ну или не доказывают. Или ошибки находят, потом поправляют, а потом всё таки доказывают...

В смысле? Оно запустит для всех k от 1 до 100000000000 при компиляции?

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

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

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

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

И я ещё обещался написать про мьютексы.

Честно говоря задачка про мьютексы не выглядит интересной для меня, поскольку там точно всё получится. Я подобное писал вот здесь https://github.com/andreykl/crosses-zeros/blob/master/Lib.idr (когда читал книжку Бреди про Идрис, там прекрасные примеры). Тут надо смотреть на тип GameCmd который обеспечивает переход игры из одного состояния в другое и при попытке перейти не вовремя, будет ошибка времени компиляции. Ну собственно этот код взять и переписать чуток да и всё.

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

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

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

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

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

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

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

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

Тут правда вопрос в практике будет... но это другой вопрос..

В Typed Racket всегда можно завернуть в cast к нужному типу, если проверялка не может доказать корректность, но программист точно уверен (в коде будет добавлена динамическая проверка на случай, если программист всё-таки неправ).

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

Но кок не про «написать любой ценой чтоб тесты прошло», а скорее про «чтобы мышь не проскользнула если умения хватит».

Функция гарантированно завершается. Сможет Coq её скомпилировать?

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

As proven by Riho Terras, almost every positive integer has a finite stopping time

almost every

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

Приведённая выше функция на коке легко формулируется, но придётся откючить проверку завершаемости.

Ты хочешь, чтобы машина решила вопрос, перед которым сдались лучшие математики современности? =)

Так точно, не известно доказательства завершимости этого алгоритма для произвольного k.

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

Мне не нравится идея, что правильный, но недоказуемый (а по Гёделю такой точно есть) код нельзя скомпилировать.

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

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

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

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

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

Но кок не про «написать любой ценой чтоб тесты прошло», а скорее про «чтобы мышь не проскользнула если умения хватит».

или лучше «чтобы мышь не проскользнула если очень надо и умения хватит»

Я же написал скорректированную функцию, которая точно завершается. Проверена завершимость до ста знаков, так что к проверке k можно ещё несколько десятков ноликов добавить.

Я же написал скорректированную функцию, которая точно завершается. Проверена завершимость до ста знаков, так что к проверке k можно ещё несколько десятков ноликов добавить.

А, я не разобрался, прошу прощения. Тем не менее, требование то же: нужно доказательство того что она завершится.

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

Если доказательство сложное, я не возьмусь. Система самостоятельно его конечно не построит.

Кстати, из любопытного
https://www.researchgate.net/publication/365435943_Proof_of_the_Collatz_Conje...

В том и дело, что она «проверена», а не «доказана».

Вы правы, в данном случае это не верная трактовка.

Специалист по логике? Программирующий на пхп? Мы с вами коллеги :) Приятно назвать коллегой специалиста по логике, пусть и коллегой по пхп :). Кстати, я вот обратил внимание (по вашей ссылке) что лямбды-то у нас таки вполне ничего выглядят теперь. А у меня стойкое ощущение осталось что я лямбды в php не люблю потому что они страшные. Может быть правда память меня обманывает и я их не люблю потому что в пятой версии их вообще не было, не знаю.. тем не мнее, сейчас вроде норм выглядит fn($value): int => $value * 2

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

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

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

о, ещё коллега :) (нет, я в курсе конечно, что нас тут добрая часть ЛОРа, но всё равно приятно общаться с умными людьми :) )

а что если реализовать паттерн command

т.е. предварительно составляется список команд, а потом они все исполняются методом execute

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

а метод execute будет валидировать корректность последовательности команд перед тем как исполнять.

кажется такое можно реализовать и с динамической типизацией

Специалист по логике?

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

Программирующий на пхп?

Где-то с 2002-2004, я не помню точно. Это один из языков который я использую почти каждый день, если и не пишу, то уж всматриваюсь прищуренным глазом точно.

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

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

написанное не очень понятно, ушёл переваривать.

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

Группа исследователей из Facebook пыталась выделить «интуицию» нахождения интеграла от функций путем обучения нейронной сети распознаванию подобных деревьев. В итоге обученная сеть очень быстро и достаточно верно (99% с чем-то) процентов справлялась с формулами которые видела впервые. Эксперимент вышел довольно удачным что аж глава отдела разработки Wolfram (делают мат пакет Mathematica) пришлось отреагировать.

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

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

В том и дело, что она «проверена», а не «доказана».

Это тоже доказательство. Перебором. Например утверждение «все нечётные натуральные числа по 7 простые» проще всего доказать перебором.

Относительно этого алгоритма, ты не прав.

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

Вот в чем дело:

Предположим, что среди чисел в диапазоне от 1 до 100000000000 есть такие, для которых алгоритм не завершится за конечное число шагов.

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

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

Так что мы зашли в тупик.

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

Ладно. Завершимость не так критична. Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)?

То есть, первый аргумент может быть «a designator for a function». То есть это функция или строка, по которой можно найти функцию. Или хотя бы число, по которому можно взять функцию из некоего массива.

Остальные аргументы должны быть гетерогенными списками. Списки могут быть разной длины. Результат будет минимальной длины из аргументов.

То есть удастся ли вообще написать что-то более конкретное, чем (на Haskell)

data Designator a b = S String | F (a -> b)
mapcar :: Designator a b -> [[Dynamic]] -> [Dynamic]

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

Nat f(Nat k) { 
  if(k == 1) return 1;
  if(k > 100000000000) return 0;
  if(k % 2 == 0) return f(k/2);
  return f(3*n+1);
}

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

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

Не скажу за coq, но в PHP это любая обезъяна сделает, как с лямбдой:

<?php
$arr1 = ['v1', 2, 'three', 4];
$arr2 = ['first', 'second', 3];

$result = array_map(fn($k, $v): string => $k." is the ".$v, $arr1, $arr2);

print_r($result);

Результат:

Array
(
    [0] => v1 is the first
    [1] => 2 is the second
    [2] => three is the 3
    [3] => 4 is the 
)

Так и без нее обычной функцией (добавил проверок на тип значения чтобы вывод был более понятный):

<?php
$arr1 = ['v1', 2, 'three', 4];
$arr2 = ['first', 'second', 3];

function describe($k, $v) {
    if (!$k) {
        $k = gettype($k);
    }
    if (!$v) {
        $v = gettype($v);
    }

    return $k." is the ".$v;
}

$result = array_map('describe', $arr1, $arr2);

print_r($result);

Результат:

Array
(
    [0] => v1 is the first
    [1] => 2 is the second
    [2] => three is the 3
    [3] => 4 is the NULL
)

Здесь всего 100000000000 состояний.

А, увидел return 0;, дошло. Чо-то у меня в голове задача переформулировалась во что-то другое и упозла от исходной, пока я делами занимался.

Кстати, это хорошая иллюстрация к тому, что несколькими страницами ранее обсуждалось:

Мы можем попытаться доказать соответствие решения некоторому набору требований, но кто сказал, что мы верно составили набор требований и не запутались. =)