Previous Up Next

Chapter 2  Математический аппарат

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

2.1  Множества, отношения и функции

Определение 1   Мы пользуемся стандартными обозначениями для множеств: фигурные скобки используются, когда элементы множества перечисляются явным образом ({…}) или когда оно задается выделением (comprehension) из другого множества ({xS ∣ … }), обозначает пустое множество, а выражение S \ T — теоретико-множественную разность S и T (множество элементов S, не являющихся элементами T). Мощность (количество элементов) множества S обозначается |S|. Множество всех подмножеств S обозначается P(S).
Определение 2   Множество натуральных чисел (natural numbers) {0, 1, 2, 3, 4, 5,…} обозначается символом . Множество называется счетным (countable), если между его элементами и натуральными числами существует взаимно-однозначное соответствие.
Определение 3   n-местное отношение (relation) на наборе множеств S1, S2, …, Sn — это множество RS1 × S2 × … × Sn кортежей элементов S1,…, Sn. Если (s1,…,sn) ∈ R, где s1S1, …, snSn, то говорится, что s1, …, sn связаны (related) отношением R.
Определение 4   Одноместное отношение на множестве S называется предикатом (predicate) на S. Говорится, что P истинен на sS, если sP. Чтобы подчеркнуть это интуитивное понятие, мы часто будем писать P(s) вместо sP, рассматривая P как функцию, переводящую элементы S в истинностные значения.
Определение 5   Двуместное отношение R на множествах S и T называется бинарным отношением (binary relation). Мы часто будем писать s R t вместо (s,t) ∈ R. Если S и T совпадают (назовем это множество U), мы будем говорить, что R — бинарное отношение на U.
Определение 6   Чтобы облегчить чтение, многоместные (трех- и более) отношения часто записываются в <<смешанном>> синтаксисе, когда элементы отношения разделяются последовательностью символов, и эти символы вместе образуют имя отношения. Например, отношение типизации для простого типизированного лямбда-исчисления из главы 9 записывается как Γ ⊢ s : T — такая формула означает <<тройка (Γ, s, T) находится в отношении типизации>>.
Определение 7   Областью определения (domain) отношения R между множествами S и T называется множество элементов sS, таких, что (s,t) ∈ R для некоторого t. Область определения R обозначается dom(R). Областью значений (codomain) R называется множество элементов tT, таких, что (s,t) ∈ R для некоторого s. Область значений R обозначается range(R).
Определение 8   Отношение R на множествах S и T называется частичной функцией (partial function) из S в T, если из (s,t1) ∈ R и (s, t2) ∈ R следует t1 = t2. Если, кроме того, dom(R) = S, то R называется всюду определенной функцией (total function), или просто функцией (function), из S в T.
Определение 9   Частичная функция R из S в T определена (defined) на аргументе sS, если sdom(R), и не определена в противном случае. Запись f(x)↑ или f(x) = ↑ означает <<f не определена на x>>, а f(x)↓ означает <<f определена на x>>.

В некоторых главах, посвященных программной реализации систем типов, нам также потребуется определять функции, которые на некоторых аргументах терпят неудачу (fail) (см., например, рис. 22.2). Важно отличать неудачу (частный случай разрешенного, наблюдаемого результата) от расхождения (divergence); функция, способная потерпеть неудачу, может быть либо частичной (т. е., может также расходиться), либо быть всюду определенной (т. е., она всегда либо возвращает результат, либо терпит неудачу) — в сущности, часто нам будет нужно доказывать, что такая функция всюду определена. Если f возвращает неудачу при применении к x, мы будем писать f(x) = неудача.

С формальной точки зрения, функция из S в T, которая может вернуть неудачу, является на самом деле функцией из S в T ∪ {неудача} (мы предполагаем, что неудача не входит во множество T).

Определение 10   Пусть R — бинарное отношение на множестве S, а P — предикат на S. Если из sRs и P(s) следует P(s′), то говорится, что R сохраняет (preserves) P.

2.2  Упорядоченные множества

Определение 1   Бинарное отношение R на множестве S рефлексивно (reflexive), если каждый элемент S связан отношением R с самим собой — то есть, для всех sS, sRs (или (s,s) ∈ R). Отношение R симметрично (symmetric), если для всех s,tS из sRt следует tRs. Отношение R транзитивно (transitive), если из sRt и tRu следует sRu. Отношение R антисимметрично (antisymmetric), если из sRt и tRs следует s=t.
Определение 2   Рефлексивное и транзитивное отношение R на множестве S называется предпорядком (preorder) на S. (Всякий раз, когда мы говорим о <<предупорядоченном множестве S>>, мы имеем в виду какой-то конкретный предпорядок на S.) Предпорядки обычно обозначаются символами  или . Запись s < t означает, что stst (<<s строго меньше t>>).

Если предпорядок (на S) к тому же антисимметричен, он называется частичным порядком (partial order) на S. Частичный порядок называется линейным порядком (total order) на S, если для любых s,tS выполняется либо st, либо ts.

Определение 3   Пусть — частичный порядок на S, а s и t — элементы S. Элемент jS называется объединением (join) (или точной верхней границей, least upper bound) s и t, если:
  1. sj и tj, а также
  2. для всякого kS, если sk и tk, то jk.

Аналогично, элемент mS называется пересечением (meet) (или точной нижней границей, greatest lower bound) s и t, если:

  1. ms и mt, а также
  2. для всякого nS, если ns и nt, то nm.
Определение 4   Рефлексивное, транзитивное и симметричное отношение на множестве S называется отношением эквивалентности (equivalence relation) на S.
Определение 5   Пусть R — бинарное отношение на множестве S. Рефлексивное замыкание (reflexive closure) R — это наименьшее рефлексивное отношение R, содержащее в себе R. (<<Наименьшее>> здесь означает, что, если имеется какое-то другое рефлексивное отношение R, включающее все пары из R, то R′ ⊆ R.) Аналогично, транзитивное замыкание (transitive closure) R — это наименьшее транзитивное отношение R, содержащее R. Транзитивное замыкание R часто обозначается R+. Рефлексивно-транзитивное замыкание (reflexive and transitive closure) R — это наименьшее рефлексивное и транзитивное отношение, содержащее R. Оно часто обозначается R*.
Упражнение 6   [★★ ↛] Дано отношение R на множестве S. Определим отношение R так:
R′ = R ⋃ { (s,s) ∣ s ∈ S }
То есть, R содержит все пары из R плюс все пары вида (s,s). Покажите, что R является рефлексивным замыканием R.
Упражнение 7   [★★ ↛] Вот более конструктивный способ определения транзитивного замыкания отношения R. Сначала определим следующую последовательность множеств пар:
    R0=R 
    Ri+1=Ri ⋃ { (s,u) ∣ для некоторого t, (s,t) ∈ Ri и (t,u) ∈ Ri
  
То есть, на каждом шаге i+1 мы добавляем к Ri все пары, которые можно получить <<за один шаг транзитивности>> из пар, входящих в Ri. Наконец, определим отношение R+ как объединение всех Ri:
R+ = 
 
i
 Ri
Покажите, что R+ на самом деле является транзитивным замыканием R — т. е., что оно удовлетворяет условиям, заданным в определении 5.
Упражнение 8   [★★ ↛] Пусть R — бинарное отношение на множестве S, и это отношение сохраняет предикат P. Докажите, что R* также сохраняет P.
Определение 9   Пусть у нас есть предпорядок на множестве S. Убывающая цепочка (decreasing chain) на есть последовательность s1, s2, s3, … элементов S, такая, что каждый элемент последовательности строго меньше предшествующего: si+1 < si для всякого i. (Цепочки могут быть конечными или бесконечными, однако для нас представляют больший интерес бесконечные, как видно из следующего определения.)
Определение 10   Пусть у нас есть множество S с предпорядком . Предпорядок называется полным (well founded), если он не содержит бесконечных убывающих цепочек. Например, обычный порядок на натуральных числах, 0 < 1 < 2 < 3 < …, является полным, а тот же самый порядок на целых числах, … < −3 < −2 < −1 < 0 < 1 < 2 < 3 < … — нет. Иногда мы не упоминаем явно и просто называем S вполне упорядоченным множеством (well-founded set).

2.3  Последовательности

Определение 1   Последовательность (sequence) записывается путем перечисления элементов через запятую. Запятая используется как для добавления элемента в начало (аналогично операции cons в языке Lisp) или конец последовательности, так и для склеивания двух последовательностей (аналогично append в Lisp). Например, если символ a обозначает последовательность 3,2,1, а символ b обозначает последовательность 5,6, то 0,a — это последовательность 0,3,2,1, запись a,0 обозначает последовательность 3,2,1,0, а запись b,a обозначает 5,6,3,2,1. (Использование запятой для двух разных операций — аналогов cons и append, — не создает путаницы, если нам не нужно вести речь о последовательностях последовательностей.) Последовательность чисел от 1 до n обозначается 1..n (через две точки). Запись |a| означает длину последовательности a. Пустая последовательность обозначается знаком или пробелом. Одна последовательность называется перестановкой (permutation) другой последовательности, если они содержат в точности одни и те же элементы, которые могут быть расположены в них в разном порядке.

2.4  Индукция

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

Аксиома 1   [Принцип обыкновенной индукции на натуральных числах] Пусть P — предикат, заданный на множестве натуральных чисел. Тогда
Если P(0)
и для любого
i, из P(i) следует P(i+1),
то
P(n) выполняется для всех n.

41ex

Аксиома 2   [Принцип полной индукции на натуральных числах] Пусть P — предикат на множестве натуральных чисел. Тогда
Если для каждого натурального числа n,
предполагая, что P(i) для всех i<n,
мы можем показать, что
P(n),
то P(n) выполняется для всех n.
Определение 3   Лексикографический (или <<словарный>>) порядок (lexicographic order) на парах натуральных чисел определяется следующим образом: (m,n) ≤ (m′,n′) тогда и только тогда, когда либо m < m, либо m=m и nn.
Аксиома 4   [Принцип лексикографической индукции] Пусть P — предикат на множестве пар натуральных чисел. Тогда
Если для каждой пары натуральных чисел (m,n),
предполагая, что P(m′,n′) для всех (m′,n′) < (m,n),
мы можем показать, что
P(m,n),
то P(m,n) выполняется для всех m,n.

Принцип лексикографической индукции служит основой для доказательств с вложенной индукцией (inner induction), когда какой-либо пункт индуктивного доказательства использует индукцию <<внутри себя>>. Этот принцип можно распространить на индукцию по тройкам, четверкам и т. д. (Индукция по парам нужна достаточно часто; индукция по тройкам иногда может быть полезной; индукция по четверкам и далее встречается редко.)

В теореме 4 вводится еще один вариант доказательств по индукции, называемый структурной индукцией (structural induction). Он особенно полезен для доказательства утверждений о древовидных структурах вроде термов или деревьях вывода типов. Математические основания индуктивных рассуждений будут подробнее рассмотрены в главе 21. Мы увидим, что все упомянутые принципы индукции являются частными проявлениями единой, более общей идеи.

2.5  Справочная литература

Тем, кому понятия, перечисленные в этой главе, оказались незнакомыми, вероятно, имеет смысл ознакомиться со справочной литературой. Существует множество вводных курсов. В частности, книга Винскела (1993) помогает развить интуицию в вопросах индукции. Начальные главы в книге Дейви и Пристли (1990) содержат замечательный обзор по упорядоченным множествам. Хэлмос (1987) служит хорошим введением в элементарную теорию множеств.

Доказательство есть воспроизводимый опыт в деле убеждения.Джим Хорнинг


Previous Up Next