Крис Окасаки
* * *
вы входите в спортивный зал, там две сотни школяров. 8 сентября - и вас мучает неодолимое желание узнать, кто же из них занимает 98-е место по росту, считая с самого маленького. нечего и мечтать о том, что вы сможете построить их по ранжиру - никто бы не смог. "Но я могу использовать QUICKSELECT!"забираетесь в самую гущу, закрываете глаза, вытягиваете руку и делаете три оборота. открываете глаза и выхватываете из толпы пацана, на которого указывает ваша рука. Петя Поворотов. кричите что есть мочи: "А ну ка! Все, кто ниже Петра - к стене! Остальным - стоять! Работает ОМОН. Те, кто одного роста с Петром могут остаться, а могут и подойти к стене. Живо!"
считаете детей у стены и детей на поле - 79 и 120. ага, нужный ребенок на поле и вы усаживаете детей у стены на скамейки. и Петю тоже
снова закрываете глаза, вытягиваете руку и крутитесь три раза. открыв глаза обнаруживате, что рука указывает на сестру Петра - Лену Поворотову. опять орете: "Быстро! Те, кто выше Лены - к стене, остальным - стоять! Тот, кто одного с ней роста могут подойти к стене, а могут и остаться на площадке"
дети вновь делятся на две группы - 60 человек у стены и 59 - на поле. ага - нужный ребенок - на поле и вы усаживаете на скамейки Лену и всех тех, кто у стенки
процедура повторяется и теперь выбран двоюродный брат Лены - Юра Поворотов. опять оставляете коротких на поле, а длинных ставите к стенке. равные могут выбирать, где им быть
суета - и вновь появляются две группы: 37 детей на поле и 22 - у стены. ага, нужный по росту ребенок - Юра. дело в шляпе
два целых числа a и b сравнимы по модулю d (d - целое), если при делении на d они дают один и тот же остаток
сравнения по модулю обладают многими свойствами обычных равенств:
т.о, сравнения по одному и тому же модулю можно складывать, вычитать и умножать
* * *
M.Масленников
понятное дело, что все делились с числом 1 - это число было вроде как Царь-Батюшка во всем множестве натуральных чисел (МНЧ). но деление с этим числом было безобидное и поэтому все натуральные числа исполняли этот религиозный обряд - деление на 1 - без каких-либо последствий для себя
ну а о другом важном числе - 0 - нельзя со 100% уверенностью сказать, что оно жило в МНЧ. у него был особняк, который все другие числа называли Конторой. все числа из МНЧ побаивались числа 0, а причина - простая. само число 0 могло делиться на кого угодно, после чего результат навсегда попадал в Контору, а вот если кто-то сам пытался делиться на 0, то его без лишних эмоций превращали в пыль. то есть число 0 жило по своим законам, отличным от законов МНЧ, и ожидать от него можно было всего, чего угодно
число 2 было хитрым. оно разделило ровно пополам всех обитателей МНЧ на тех, кто с ним делился, и тех, кто это делать категорически отказывался. первых число 2 называло честными и даже создало из них партию: Партию Честных Чисел. в партии было Политбюро из наиболее известных честных чисел: 2, 4, 6 и 8. параграф 1 Устава гласил, что в партии могут состоять любые числа, признающие Устав и Программу и оканчивающиеся на одного из членов Политбюро. Устав приняли под бурные и продолжительные аплодисменты, но когда число 2 принесло его на согласование в Контору, там параграф 1 дополнили: "и 0". так его и утвердил Царь. а Программа у партии была простая: наша цель - бесконечность
за числом 3 закрепилась - как бы это поделикатнее сказать - отличная от числа 2 репутация. как соберутся числа отметить какое-нибудь событие, так обязательно разобьются на группы по три числа в каждой. почитателей у числа 3 было достаточно. вместо красных носов у чисел ходило такое правило: число является алкоголиком, если сумма его цифр - алкоголик
число 5 было безобидно, партий своих создавать не пыталось, а на выборах всегда выдвигалось от единого и нерушимого блока честных и беспартийных. делились на него те, у кого на конце было 5. "или 0" - дополнили в Конторе
но были в МНЧ и диссиденты: числа, не вступившие в партию, и вообще, не желавшие ни с кем делиться, кроме Царя. в народе их называли простыми числами. строго говоря, и всеми уважаемые числа 2, 3 и 5 тоже были простыми, но благодаря куче поклонников - других чисел из МНЧ, которые с ними делились, - Царь считал их «своими» и никаких репрессий к ним не применял. а вот числу 13 не повезло: оно жило рядом с честным-пречестным числом 12 и постоянно пыталось отучить его от алкоголизма. как бы не так! число 12 написало в Контору, после чего отдел Пропаганды объявил число 13 причиной всех бед и несчастий в МНЧ и обозвал его «чертовой дюжиной»
так и жили тысячу лет в МНЧ, умножались и делились, стремясь достигнуть светлой цели - бесконечности, но никак не могли этого сделать. и партийные вожди однажды провозгласили перестройку: «давайте делиться с остатком!». а народ в МНЧ был такой, что палец ему в рот не клади - руку по локоть откусят. все сразу смекнули, что остаток-то - штука неплохая. главное, чтобы он в 0 не обратился. и вот ведь что еще негодяи придумали - конечные группы. до того всем числам на всех политзанятиях только и внушали: наша цель - бесконечность, а тут - упала дисциплина, перестали слушать партийных пропагандистов, а на улицах стали появляться антиправительственные листовки:
Наша цель - конечная группа!
Всем! Всем! Всем!
Натуральные числа! Не слушайте пропагандистов из партии честных чисел - врут они нам, что наша цель - бесконечность. Наша цель - конечная группа!
Вам забивают голову этой мистической бесконечностью, а мы расскажем вам, как быстро создать реальную конечную группу.
Выбирайте себе модуль, умножайтесь и делитесь на него с остатком! Частное выбрасывайте, а остатки образуют конечную группу.
Нет бесконечности!
Контора сперва хотела принять радикальное решение: показать всем этим вольнолюбцам настоящую бесконечность, обратив их в пыль, но хитрое число 2 надоумило Контору не делать глупостей, а действовать тоньше и с выгодой для себя. надо просто подсунуть горлопанам подходящий модуль. например, честного-пречестного алкоголика - число 12
идет как-то на нетвердых ногах число 3, а навстречу ему прямо сияет честное-пречестное число 8
- Давай вступим в конечную группу по модулю 12
- Давай!
вступили. перемножились. раньше такое сколько раз вытворяли - и в Контору за это никто не попадал. а тут как только привели результат по модулю 12, глазом не успели моргнуть, как он уже в Конторе
- Ну что, сынки, помогло вам ваше деление с остатком?
приуныли натуральные числа. неужели опять - все по-старому, наша цель - бесконечность? а нельзя ли как-то получить другую конечную группу? день думали, два, а на третий вспомнили о простых числах, тех, которые ни с кем не делятся. взяли соседа числа 12 - затравленное число 13. и, о чудо! кто с кем в его конечной группе ни умножался по модулю 13, а результат в Контору так и не попал!
и стали в МНЧ очень популярны числа, которые не хотели ни с кем делиться. как только выберут такое число модулем, так в его конечной группе законность и порядок, все арифметические операции выполняются четко и правильно. а нулю в этой группе места уже не было
Контора была в ярости. это кто ж теперь в модулях ходит? без 0 в конце, беспартийные, непьющие, без юбилейных медалей! по-обычному ни с кем не делятся - простые! да таких простых - раз два - и обчелся! а как же светлое будущее? с кем его строить-то будем, если все простые закончатся?
- Не закончатся - ответил Конторе старик Эратосфен
но на всякий случай в Конторе решили поставить все конечные группы на учет, под буквой Z (от слова zero - агентурной клички числа 0):
Z/2 - группа по модулю 2,
Z/3 - группа по модулю 3
и так далее
группа Z/2 была совсем неинтересной и состояла из одного Царя-Батюшки - числа 1
группа Z/3 состояла из Царя и партийного Вождя - числа 2. забавные превращения там получались. партийный Вождь, перемножившись сам с собой, превращался в Царя - ну это еще можно понять, такие превращения бывали. а вот Царь-то, Царь - хорош гусь! поделившись на партийного Вождя, сам становился партийным Вождем!
вскорости из конечных групп стали создавать ночные клубы: «Семеро козлят», «Футбольная команда», «Чертова дюжина», «17 мгновений весны» и прочая, прочая, прочая. натуральные числа были рады их появлению. особенно рад был Царь-Батюшка. сидит, бывало, в своем дворце целыми днями один-одинешенек, и поделиться-то не с кем, ни на кого он не делился. а тут, в конечной группе - делись с кем хочешь, хоть до утра. и число 2 меньше стало внимания уделять своей партии - надоели, зануды. пойдут, бывало, Царь вместе с партийным Вождем в weekend в какие-нибудь «Мгновения» душу отвести, наделиться всласть на всю трудовую неделю вперед, а там уже и число 3 (меньше пить стало) и 5 (без медалек) и 12 (подружившееся с 13) - все веселые, друг с другом делятся. какие тут партии и партбилеты! без особых проблем число 2 согласилось на переименование своей партии в множество - множество четных чисел
... поскипано мышами ...
... а вот RSA как раз и стал таким алгоритмом, в котором без простых чисел обойтись никак невозможно. только простые числа для RSA нужны большие - ведь они же секретный ключ! думало - думало об этом число 2 и решило, что длина простого числа в RSA должна быть 512 или 1024 бит. "пол-литра и литр" - по-своему расшифровало эти значения число 3
и брошен был клич: все на поиски больших простых чисел, ибо без них не будет в МНЧ ни Internet Banking, ни электронной коммерции. а простые числа - скромные, тихо сидят себе по своим конечным группам, никаких явных признаков у них нет. как их отыскать во множестве натуральных чисел? задачу эту поручили Конторе, ну а Контора выполнила это поручение так, как умела. переписали в Конторе все простые числа до 256 и поехали по отдаленным уголкам необъятного МНЧ. случайно заезжают в какую-нибудь глухомань и хватают там первого попавшегося аборигена
- Говори, падла, с кем делишься?
- Гражданин начальник, ни с кем не делюсь.
- Врешь, гад!
- Век бесконечности не видать!
и тут конторские начинают его делить на все припасенные простые числа, да при каждом делении запятую к заду норовят приставить. отвалилась запятая - врет, делится. но даже если выдержал мужичок все эти пытки, то Контора на этом не успокаивается
- Говори, паскуда, сколько у тебя свидетелей простоты?
и вот только после того, как найдет m-мужичок достаточное (log2m) число свидетелей своей простоты, сажают его в машину и везут в столицу: RSA-ключом будет
всю эту процедуру прозвали в народе тестом Миллера-Рабина. вылавливают конторские таким образом пару пол-литровых мужичков - числа p и q, и готов секретный ключ. перемножают их, получают литровый открытый ключ - n, который затем одевают в нарядный сертификат
и, надо признаться, даже несмотря на эту процедуру, чисел, желающих вырваться из деревенской глуши в столицу в качестве RSA-ключей было предостаточно. а о том, чтобы всех их просто пересчитать, не говоря уже об опробовании, не могло быть и речи - слишком много. поэтому алгоритм RSA для пол-литровых и литровых простых чисел был признан стойким
* * *
x² + b * x + c = 0 x² + b * x = -c x² + b * x + b² / 4 = b² / 4 - c (x + b / 2)² = (b² - 4 * c) / 4 x + b / 2 = ± √ (b² - 4 * c) / 2 x = [-b ± √ (b² - 4 * c)] / 2
x = a ^ loga x = loga (a ^ x) loga x logb x = ------- loga b loga x + loga y = log a (x * y) loga (x ^ y) = y * log a x
e = lim (1 + 1/n)n n → ∞ exp x = lim (1 + x/n)n n → ∞ (ln x)' = 1/x ∫ ln x dx = x * (ln x - 1)
1 + 2 + ... + n = n * (n + 1) / 2 = n2/2 + n/2 f(n) = Ο(n2) 1² + 2² + ... + n² = n * (n + 1) * (2 * n + 1) / 6 f(n) = Ο(n³)
в Maxima :
(%i11) load (functs) ; (%i24) arithsum (1,1,3) ; (%o24) 6
q0 + q1 + q2 + ... = 1 / (1 - q), 0 < q < 1
пример:
1 + 1/2 + 1/4 + 1/8 + ... = 1 / (1 - 0.5) = 2
в Maxima :
(%i11) load (functs) ; (%i17) geosum (1,0.5,inf) ; (%o17) 2.0 (%i18) geosum (1,0.9,inf) ; (%o18) 10.0
1 + x + x2 + x3 + x4 + ... + xn = (1 - xn+1) / (1 - x), x ≠ 1
желая установить справедливость некоторой общей теоремы A при любых значениях n, мы доказываем эту теорему последовательно для бесконечного ряда специальных случаев A1, A2, ...
возможность этого рассуждения покоится на двух предпосылках:
предположим, что требуется установить справедливость бесконечной последовательности математических предложений A1, A2, A3, ..., которые все, совместно взятые, образуют некоторое общее предложение A. допустим, что:
a well-known scientist once gave a public lecture on astronomy. he described how the earth orbits around the sun and how the sun, in turn, orbits around the centre of a vast collection of stars called our galaxy. at the end of the lecture, a little old lady at the back of the room got up and said: “What you have told us is rubbish. The world is really a flat plate supported on the back of a giant tortoise”. the scientist gave a superior smile before replying, “What is the tortoise standing on?” – “You’re very clever, young man, very clever”, said the old lady, “But it’s turtles all the way down!”
(из Курранта)
n ∈ N
предикат: P (инвариант)
базовый случай: P(k) , k < n (частные случаи: k = 0, k = 1)
вывод: if P(n) == True then P(n+1) == True
n ∈ N
предикат: P (инвариант)
базовый случай: P(k) , k < n (частные случаи: k = 0, k = 1)
вывод: if ∀ k : k ≤ n, P(k) == True then P(n+1) == True
есть какой-то предикат P(x), и для него известно, что
такие вещи существуют. эти идеи развивали, в частности, Есенин-Вольпин и Вопенка. у последнего есть книга "Математика в альтернативной теории множеств", где всё строится на базе понятия "конечного", а эффект бесконечного имитируется при помощи "парадокса кучи", т.е. принцип индукции имеет ограниченную применимость. конечный "неклассический" натуральный ряд представляется в виде 1,2,...,ℵ, где ℵ - мифическое "очень большое число", до которого "нельзя досчитать". при этом аксиомы несколько варьируются. противоречие с принципом индукции возникает, но вывод такого противоречия может быть получен не раньше, чем мы досчитаем до ℵ, а поскольку про ℵ ничего не известно, то происходит имитация эффекта бесконечного. "неклассические" натуральные ряды также имеют некоторое отношение к проблеме вычислений за реальное время. скажем, можно разрешить не все рекурсивные функции, а только растущие не слишком быстро
арифметику Пеано на самом деле тоже не очень тестировали - "больших индукций" в математической практике мало - реальная математика живет в маленьком кусочке. если удастся всю "повседневную математику" погрузить в более слабую теорию, то, во-первых, непротиворечивость PA станет не важна, а во-вторых, в противоречивость будет гораздо легче поверить. консистентность аксиоматики Пеано была доказана в расширенной системе аксиом (с трансфинитной индукцией и, кажется, чем-то ещё), но какой смысл в этом доказательстве, если нет (и не может быть) доказательства консистентности этой расширенной системы? ведь получается, что это доказательство нисколько не добавило нам уверенности в том, что PA непротиворечива
собственно, колмогоровская сложность уже является вещью сомнительной для последовательного конструктивиста, и потому ее формализация в PA должна, скорее всего, содержать "неестественные" этапы. в терминах "ультрафинитизма" вообще нельзя рассматривать то, что называют "стандартной моделью" PA. в идеях Есенина-Вольпина как раз нет ничего "мистического". более того, он как раз пытался обосновать непротиворечивость даже ZF на базе построения её "как бы модели" на базе "как бы конечного". многие его соображения уже давно реализованы (хотя бы у Вопенки). там проблема скорее не в "экзотичности" или "неправдоподобии", а в том, что "неформальные" идеи не доведены до конца
листинг Coq
"Big-O" ignores data storage latencies, topology, volume, available memory, and even the computational cost of every CPU instructions involved in a given implementation – instead, it merely counts the number of algorithmic operations. "Big-O" can be a valuable indication when designing algorithms but the best performing and scaling solution depends on the particular constraints of any specific problem and environment
f(n) - асимптотически неотрицательна
асимптотически точные оценки
f(n) = Ο (g(n)) | ∃ c > 0, n0 > 0 | 0 ≤ f(n) ≤ c * g(n), if n > n0 | lim f/g < ∞ |
f(n) = Θ (g(n)) | ∃ c1 > 0, c2 > 0, n0 > 0 | 0 ≤ c1 * g(n) ≤ f(n) ≤ c2 * g(n), if n > n0 | 0 < lim f/g < ∞ |
f(n) = Ω (g(n)) | ∃ c > 0, n0 > 0 | 0 ≤ c * g(n) ≤ f(n), if n > n0 | lim f/g > 0 |
асимптотически неточные (граничные) оценки
f(n) = ο (g(n)) | ∀ c > 0, ∃ n0 > 0 | 0 ≤ f(n) ≤ c * g(n), if n > n0 | lim f/g = 0 |
f(n) = ω (g(n)) | ∀ c > 0, ∃ n0 > 0 | 0 ≤ c * g(n) ≤ f(n), if n > n0 | lim f/g = ∞ |
нельзя использовать асимптотическую нотацию в предикатах матиндукции. предикат - это скаляр, а нотация применима только к функциям
T (n) = k * T (n / m) + f (n)
где
T - время решения задачи от аргумента
k - число подзадач
m - величина дробления на подзадачи
f - нерекурентный член
выписываем рекурентное соотношение в виде:
общее время -------> T(n) = a * T(n / b) + f(nc) <------ нерекурентное слагаемое
_ _____
^ ^
кол-во частей ----------+ |
размер одной части ------------------+
оцениваем нерекурентную часть f(nc) по параметрам рекурентной и получаем оценку работы алгоритма:
если оценка для c есть: | то оценка для всего алгоритма есть: |
---|---|
log b a > c | T(n) = Θ(nlog b a) |
log b a = c | T(n) = Θ(nc log n) |
log b a < c | T(n) = Θ(f(nc)) |
выписываем рекурентное соотношение в виде:
T(x) = Σ [ak * T (bk * x)] + f(x) kгде
x T(x) = Θ (xp * (1 + ∫ [f(x)/x^(1+p)] dx)) 1где
p ∈ R : Σ ak * bkp = 1 k
алгебры с несущим множеством, состоящим из двух элементов называют бинарными. операции, общие для всех таких алгебр:
существуют и другие операции, как унарные, так и бинарные. всего может быть 16 бинарных операций (число подмножеств есть 2^2 = 4 и соответственно, число операций 2^4 = 16) и четыре унарных (2^1 = 2 и, соответственно, 2^2 = 4)
эти двадцать операций позволяют строить новые функции путем подстановки. функцию, полученную путем применения (возможно многократного) подстановок, называют суперпозицией
дизъюнкция конституент единицы, равных единице на тех же наборах, что и заданная функция, называется совершенной дизъюнктивной нормальной формой функции
(~A /\ B) \/ (A /\ ~B)
коньюнкция конституент нуля, которые равны нулю на тех же наборах, что и заданная функция, называется совершенной конъюнктивной нормальной формой функции
(~A \/ ~B) /\ (A \/ B)
любая функция, полученная с помощью операций подстановки из функций данного класса, обязательно будет принадлежать к тому же классу
система функций называется полной, если с помощью функций, входящих в эту систему, применяя операции подстановки, можно получить любую функцию. для того чтобы система была полной, необходимо и достаточно, чтобы она включала:
система функций называется независимой, если ни одна из входящих в нее функций не выражается через другие функции этой же системы с помощью подстановки аргументов
множество из двух атомов { true , false } c определенными на нем операциями отрицания, конъюнкции и дизъюнкции образует Булеву алгебру
{ true , false } , ~_ , _/\_ , _\/_
если же в качестве операций взять коньюнкцию, сложение по модулю два и единичную операцию, то получим алгебру Жегалкина
{ true , false } , _/\_ , _⊕_ , 1_
на ее основе строятся полиномы Жегалкина и каждая функция единственным образом представляется в виде такого полинома. такое представление называется алгебраической нормальной формой
1 ⊕ a ⊕ c ⊕ (a /\ b) ⊕ (a /\ b /\ c)
представление функции в алгебраической нормальной форме позволяет сразу же определить, линейна исходная функция или нет
логическое исчисление, заданное посредством некоторого множества аксиом и некоторого множества правил вывода, называется гильбертовским исчислением. теоремами исчисления называются любые формулы, которые могут быть получены из аксиом исчисления в результате применения (возможно, многократного) указанных правил. если формула А выводима из некоторого множества Г исходных посылок, то тогда запись принимает вид
Г |- Атакая запись значит, что А есть теорема
простейшей моделью является логика высказываний
высказывание – это утверждение. высказывание, значение которого может быть только true или false, можно рассматривать как предикат с арностью ноль. для построения сложных высказываний используются логические операции (формулы) бинарной алгебры
утверждающий модус, Modus Ponens A -> B, A --------- B отрицающий модус, Modus Tollens A -> B, ~A ---------- ~B транзитивность A -> B, B -> C -------------- A -> C закон противоречия A -> B, A -> ~B --------------- ~A объединение посылок A -> (B -> C) --------------- (A /\ B) -> C разъединение посылок (A /\ B) -> C --------------- A -> (B -> C) intro конъюнкции A , B ------ A /\ B elim конъюнкции A /\ B A /\ B ------ ----- A B intro дизъюнкции A B ----- ------ A \/ B A \/ B
листинг Agda (с предыдущим модулем ):
законы деМоргана ~(A \/ B) <=>(~A /\ ~B) ~(A /\ B) <=>(~A \/ ~B) закон контрапозиции (A => B) <=>(~B => ~A) поглощение A \/ (A /\ B) <=>A A /\ (A \/ B) <=>A дистрибюция A /\ (B \/ C) <=>(A /\ B) \/ (A /\ C) A \/ (B /\ C) <=>(A \/ B) /\ (A \/ C)
листинг Agda (с предыдущим модулем):
аксиома исключённого третьего (лат. tertium non datur, то есть «третьего не дано») — закон классической логики, состоящий в том, что из двух высказываний — «А» или «не А» — одно обязательно является истинным, то есть два суждения, одно из которых формулирует отрицание другого, не могут быть одновременно ложными
с конструктивистской точки зрения, установление истинности высказывания вида «А или не А» означает:
в конструктивной математике суждение считается истинным, только если оно доказывается ПОСТРОЕНИЕМ ТАКОГО ОБЪЕКТА. поскольку, вообще говоря, не существует метода, позволяющего для любого высказывания за конечное число шагов установить его истинность или истинность его отрицания, закон исключённого третьего не должен применяться в рамках конструктивного направления как аксиома, ибо
1. имеются утверждения о наличии элементов в бесконечных множествах, которые никак невозможно проверить на их конечных частях. и они могут оказаться недоказуемыми. это связано с неразрешимостью
2. сам способ порождения доказательств может быть настолько сложен, что будет моделировать задачи из общей рекурсии, про которые уже известно, что они неразрешимы
но это все зависит от выбранной аксиоматики. в более слабых теориях возможны чудеса
на компьютере же нет бесконечных множеств. например, размер расчитанного числа π не сможет превысить размер памяти компьютера. вот и получается, что компьютерные науки про одно, а математические арифметики про другое. то есть на компе всё разрешимо. комп может разрешить, что для термов длины меньше K, что-то так или не так. то есть, не вообще решить, а скажем так, сообщить, что простого решения (умещающейся в память компов) точно нет. а ведь может оказаться, что решение, это скажем, что-то по схеме бесконечной, но есть и компутеру это не сообразить. но вот только для термов длины, которые умещаются в память сейчашных компов, ниччо доказать не смогут вот так вот, простым перебором. то же самое можно сказать и про разрешимое, но экспоненциально-стопицотой степени
с другой стороны - разрешимость и даже complexity являются математическими игрушками. представьте что надо написать программу, создающую будку на Х собак, где Х - натуральное. но задача не решаема в общем виде! на 1-2 собаки надо делать классическую будку, на 3-10 - вольеры из сетки в ряд, а на большее число - уже целые комплексы т.к. надо решать совершенно другие проблемы (вроде массового выгула). но точно такая же ситуация например с задачей коммивояжёра. при некоторых размерах она тривиальным циклом решается, при некоторых требует распараллеливания, при некоторых требует суперкомпьютера с хорошим интерконнектом, а при некоторых вообще не имеет физического смысла т.к. ждать ответа придется годы
у Тани в кармане икс конфет, а у Вани эн-большое. как им поделить лакомства по справедливости, если у Тани конфеты Прессбургера, а у Вани - примитивно-рекурсивные
а возвращаясь к закону исключенного третьего, можно резюмировать: конструктивисты изучают то, что доказываемо, в то время как классическая логика изучает, что является "истинным"
в современных реализациях отрицание реализовано для всех населенных типов, как ненаселенный тип False
. предьявить доказательство из ненаселенного типа не представляется возможным и потому для любого реализованного типа P отрицание терма p : P , ¬ p
будет термом из ненаселенного типа, то есть - его не будет. закон исключенного третьего в программировании не работает
с точки зрения программиста отрицание классического закона исключенного третьего означает, что мы не сможем скомпилировать программу, содержащую такие две функции:
Haskell
data Void lemma :: Either a (a -> Void) lemma = undefined -- doubleNeg :: forall a. a -> a doubleNeg :: ((a -> Void) -> Void) -> a doubleNeg = undefined
для второй нам придется выбирать либо использовать терм с типом (a -> Void) -> Void
или обходиться без него - что равнозначно использованию конструкции forall a. a
, которая по определению незаселена. и тут мы застряли! но та же самая история и с функцией lemma - чтобы она скомпилировалась, нужно удовлетворить те же самые условия, что и для двойного отрицания
в булевой логике любое утверждение либо истинно, либо ложно, его можно просто заменить одной из этих двух констант. в конструктивной логике жизнь разнообразней. есть разница между true и irrefutable
утверждение истинно, когда у меня есть его конструктивное доказательство в виде конкретного объекта, программы. пока такое доказательство не получено, утверждение не истинно, но и не ложно, оно просто еще не решено
ложно оно тогда, когда у меня опять же есть конкретная программа, которая из предполагаемого док-ва этого утверждения производит ⊥, виснет. ложные утверждения - это типы плохих, негодных, виснущих программ
наконец, irrefutable оно, когда его отрицание ложно. т.е. у нас нет конструктивного доказательства данного утверждения, мы не называем его истинным, но у нас есть конструктивное доказательство, что предположение о его ложности ведет к абсурду, т.е. его отрицание ложно
есть определенная процедура, позволяющая конвертировать классические доказательства в конструктивные, но не один в один, а ценой замены для некоторых утверждений истинности на бесспорность (так по русски irrefutable?). если конкретнее, в импликациях перед следствиями появляются двойные отрицания
классическая логика получается из интуиционистской факторизацией по ¬¬А = А, то есть классическая логика - это некоторая подтеория интуиционистской логики, которая содержит только формулы вида ¬¬А. но поскольку ¬¬ у нас стоит перед каждой формулой, то мы его в классике опускаем. значит, "А" в классической логике имеет ту же семантику, что и "¬¬А" в интуиционистской, а "А" интуиционистской вообще ни чему в классической не соответствует. вообще, это же (что мы можем исследовать классические утверждения в рамках интуиционизма, как следствие) интереснейший факт, но как-то почему-то особого никто внимания на нем не заостряет никогда
до того как появились компьютеры, проблема разрешимости (Entscheidungsproblem) стимулировала создание множества равноценных определений «вычислимости»:
многие из них соответствуют методам программирования, несмотря даже на то, что они появились раньше компьютеров
todo
в "логике высказываний" мы рассматриваем операции над высказываниями (арность каждого высказывания равна нулю), а теперь переходим к операциям с использованием "предикатов"... но что такое "предикат"?
предикат – это функция одного или нескольких переменных
P (x1 , x2 , ... , xn) = true | false
результат можно рассматривать как высказывание о наличии отношений между аргументами предиката. сами эти аргументы не обязаны быть бинарными, а могут принимать значения из множества (в том числе и бесконечного); причем для разных аргументов предиката эти множества могут быть разными
итак, предикат - это функция с булевым значением. функция - она однозначно отображает множество аргументов на область значений. значений у предиката - только два, но "предикат", в отличие от "высказывания"
над предикатами можно проделывать те же самые логические операции, что и над высказываниями. принципиальное отличие от логики нулевого порядка заключается в том, что предикат представляет из себя множество экземпляров, которые определяются значениями аргументов, между тем как высказывания строго фиксированы двумя экземплярами
другим отличием от логики нулевого порядка является использование не только булевых связок, но и кванторов существования и общности
листинг Agda (с предыдущим модулем)
операцией связывания квантором общности называется правило, по которому каждому предикату P(...,x,...) сопоставляется высказывание, обозначаемое ∀x.P(...,х,...), которое истинно в том и только в том случае, когда предикат Р тождественно истинен при любом x, и ложно в противном случае. в выражении ∀x.P(...,х,...) переменная х уже перестает быть переменной, то есть вместо нее невозможно подставить какие бы то ни было конкретные значения, так как необходимо, чтобы условие выполнялось для всех значений x. говорят, что переменная x связанная
операцией связывания квантором существования называется правило, по которому каждому предикату Р(...,х,...) сопоставляется высказывание, обозначаемое ∃x.P(...,x,...), которое ложно в том и только в том случае, когда предикат P тождественно ложен для любого значения x. в выражении ∃x.P(...,x,...) переменная х перестает быть переменной: это связанная переменная, так как необходимо, чтобы условие выполнялось
если на предикат навешивается квантор, то фактически (из-за связывания переменной) этот предикат уменьшает свою арность на единицу. если навесить по квантору на каждую переменную, то предикат превратится в "высказывание"
на многоместные предикаты можно на разные переменные навешивать различные кванторы. нельзя на одну и ту же переменную навешивать сразу два квантора
итак, переменная, на которую навешен квантор, называется связанной; несвязанная квантором переменная называется свободной. выражение, на которое навешивается квантор, называется областью действия квантора и все вхождения переменной, на которую навешен квантор, в это выражение являются связанными
взяв любое множество S, мы можем задать для него предикат χ такой, что:
χ(x) = (true if x ∈ S, false if x !∈ S)и для любого унарного предиката P, мы можем рассмотреть множество всех x, удовлетворяющих
P(x) = trueтаким образом, множества и предикаты являются лишь различными способами выражения одних и тех же понятий: вместо трактовки S как множества и записи x ∈ S, мы можем рассматривать его как предикат и записывать как S(x)
для кванторов (в классической логике) выполняются:
∀x . P(x) = ~ (∃x . ~ P(x)) ∃x . P(x) = ~ (∀x . ~ P(x))
на интервале (конечной области) - это аналоги законов деМоргана. на двух обьектах это в точности законы деМоргана
∀x . (P1(x) /\ P2(x)) = ∀x . P1(x) /\ ∀x . P2(x) ∃x . (P1(x) \/ P2(x)) = ∃x . P1(x) \/ ∃x . P2(x) ∃y . ∀x . P(x,y) => ∀x . ∃y . P(x,y)
листинг Agda (с предыдущим модулем):
число подмножеств множества с кардинальностью n :
k = 2 ^ n
число перестановок множества с кардинальностью n :
k = n!
(n, k) = n! / [k! * (n - k)!]
(n, k1 k2 .. kr) = n! / [k1! * k2! * ... * kr!]
n! ∼ ( 2 * π * n )1/2 * ( n / e )n
сумма любого ряда есть степень соответствующей вершины графа (число ребер, сходящихся в этой вершине)
сумма любого столбца есть 2
сумма любого ряда есть разность входящих/выходящих ребер соответствующей вершины графа
сумма любого столбца есть 0
при наличии ребра из вершины i в вершину j значение элемента wij равно 1, а при отстутствии ребра равно 0
сумма любого ряда|столбца есть степень соответствующей вершины графа (число ребер, сходящихся в этой вершине)
неориентированная смежная матрица (ненаправленного) графа всегда симметрична и поэтому все собственные вектора такой матрицы - вещественны. они представляют ортогональный базис диапазона
множество собственных значений смежной матрицы называется спектром графа
на главной диагонали смежной матрицы графа без петель всегда будут нули ("петля" - ребро
если M - смежная матрица графа, то любой элемент xij матрицы Mn - число путей длины n из вершины i в вершину j
матрица расстояний графа имеет значением каждого своего элемента xij минимальное количество ребер на пути из вершины i в вершину j
пусть di - степень вершины i - число входящих/выходящих ребер.
Лаплассиан графа есть квадратная матрица:
Lij = di if i==j | -1 if vivj ∈ egde | 0 otherwise
Лаплассиан может быть получен из смежной матрицы M путем несложной замены, с последующей операцией умножения и транспонирования
сначала в каждом столбце j матрицы M заменяем:
и затем полученную таким образом матрицу S транспонируют и перемножают
L = S * S⁺
наименьший ненулевой собственный вектор Лапласиана называется спектральным разрывом
спектральный разрыв равен нулю тогда и только тогда, когда граф несвязен (есть изолированные вершины)
сложностью графа называется число, равное произведению ненулевых собственных чисел Лапласиана деленное на число вершин
c = Π λi / n
сложность - это число спан-деревьев графа
Лаплассиан еще называют матрицей Кирхгофа или admittance matrix
если граф является деревом, то Dij = det L(i,j) (при числе вершин больше двух)
путь, содержащий все ребра, причем каждое ребро входит в путь единожды
связный граф содержит путь Эйлера тогда и только тогда, когда все его вершины имеют четные степени
листинг Haskell
путь, содержащий все вершины, причем каждая вершина входит в путь единожды
любой турнирный (расщепленный, m = n >= 2, связный) граф содержит путь Гамильтона