Архитектура системы верификации кода драйверов Linux

> То что [ℕ] несчётный это то что Кантор доказывал (про действительные числа и диагональный аргумент).

бугага

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

вообще множество конечных программ на хаскеле счетно, и множество тиков таймера тоже счетно — как ты собрался с их помощью пересчитать несчетное множество?

я уже сказал, что рассматриваю ... языки

ЯП тут вообще ни при чём, это чистая математика. В реальности вообще память ограничена.

вообще множество конечных программ на хаскеле счетно, и множество тиков таймера тоже счетно — как ты собрался с их помощью пересчитать несчетное множество?

Вот я и говорю, ADT это язык (не ЯП, а формальный математический язык) для конструктивного задания множеств и мощности задаваемых множеств нужно оценивать строго в математическом смысле. Есть другие языки (inductive families, категорное задание множеств), при этом говорить «множество всех ADT счётно» нельзя, можно сказать, что множество ветвей у данного switch/case счётно если они работают на (воображаемой) машине с бесконечной памятью, или что на машине с конечной памятью в рантайме мы можем аллоцировать только конечное количество объектов разных типов данных, ну и т.п.

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

Мой парсер, мой парсер!1 :)

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

прекрасно

1. алфавит этого формального математического языка, надеюсь, конечен? (да/нет)

2. этот язык допускает слова только конечной, но сколь угодно большой длины? (да/нет)

Мы будем говорить о мощности множества термов данного ADT?

Тогда несчётны по крайней мере:

• Множества всех инфинитных строк на финитных алфавитах (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁).
• Множества всех инфинитных строк на инфинитных алфавитах (ℵ₀ ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁). Например, можно взять счётные целые числа, счётное множество простых чисел и построить несчётное множество действительных чисел как сепарабельное декартово пространство (следуя основной теореме арифметике которая тут совпадёт с теоремой об однозначности разложения вектора по ортам в декартовом пространстве).
• Всех финитных n-арных деревьев (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁).
• Всех n-кортежей финитных строк на финитных алфавитах (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁). ℝ в виде записи с целой и дробной частями как раз такой 2-кортеж, для которого применим диагональный аргумент.

В последних двух пунктах у нас даже обычные (финитные) структуры (деревья, строки и кортежи). Вот ещё ссылка на тему - http://okmij.org/ftp/Computation/uncountable-sets.html.

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

А ∞-арные деревья и ∞-кортежи это, видимо, ℵ₀ ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁

сколько неизоморфных ADT задаётся с помощью языка задания ADT

И про inductive families тогда не забыть, они интереснее.

далее слово финитный я понимаю как «имеющий конечное число элементов»

Тогда несчётны по крайней мере ... множества ... Всех n-кортежей финитных строк на финитных алфавитах

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

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

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

заметим, что это работает, даже если n у тебя не фиксировано, и ты неявно подразумевал «объединение по всем натуральным n множеств всех n-кортежей финитных строк на финитных алфавитах»

Всех финитных n-арных деревьев

я полагаю над конечным алфавитом? ну пусть даже и над счетным, не важно

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

точно так же добавим в алфавит три символа "(" ")" "," и запишем каждое дерево в виде (вершина,ветвь,ветвь,ветвь), где каждая ветвь тоже в свою очередь дерево или элемент алфавита

в результате — опять мы представили каждый элемент Несчетного По Квазимото Множества в виде конечной строки над конечным алфавитом

какое несчастье :-(

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

дробная часть это не финитная строка

короче, ты порешь полную чушь

Тогда несчётны по крайней мере: Множества всех инфинитных строк на финитных алфавитах

детский саааааааад

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

Про деревья - множество всех бинарных деревьев изоморфно множеству финитных и инфинитных бинарных строк, мощность которого = мощность континуума. Или так - берём бинарное дерево n-ой глубины, тогда количество его поддеревьев, т.е. бинарных деревьев глубиной до n это, с точностью до коэффициентов, 2 ^ n, тогда в пределе деревьев до счётной глубины получаем 2 ^ ℵ₀ = мощность континуума.

детский саааааааад

Ага. Вот есть множества, есть их мощности, отрицать, что тут возникают как множества счётной мощности так и множества с мощностью континуума (чисто формально) нельзя - это так.

да, несчетны, но как это связано с моей попыткой решения задачи верификации для АлгТД?

Про покрытие всех clauses мы уже решили (и сказали, что haskell/agda так умеют, а agda ещё и Fin типы умеет). А про счётность ADT - хотя это и не имеет практического значения, говорить «множество всех ADT счётно» нельзя. Можно сказать «нам нужно только счётное множество ADT», или «case осуществляет выбор по счётному количеству вариантов», хотя даже это имеет чуть более чем никакое практическое значение :)

дробная часть это не финитная строка

Точно. Про «n-кортежи финитных строк на финитных алфавитах» ступил. Но всё ещё остаются инфинитные строки и финитные (!) деревья :)