Математические модели вычислений

Нормальные алгорифмы Маркова. Язык программирования Рефал. Суперкомпиляция.

λ-исчисление Чёрча. Рекурсивные комбинаторы и парадоксы.

λ-исчисление с простыми типами. Свойство сильной нормализации.

maxim.krivchikov@gmail.com

https://maxxk.github.io/formal-models/

Алгорифмы Маркова

Пусть задан конечный алфавит A, не содержащий символов «перевод строки» (γ), «→» и «→.». Нормальным алгорифмом назовём последовательность формул подстановки вида:

< строка A^* > (образец) → < строка A^* > (результат)

< строка A^* > → . (останов) < строка A^* >

На вход алгорифма подаётся строка A^*. Далее для каждого правила по порядку выполняется поиск образца в строке слева.

Если образец найден, т.е. для правила L → D входная строка T представлена в виде T = R · L · S, то подстрока L заменяется на D и результатом шага объявляется строка T' = R · D · S. Если стрелка — стрелка останова, то выполнение завершается с результатом T', в противном случае выполняется следующий шаг (просмотр образцов сначала).

Если образец не найден, переходим к следующему правилу.

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

Примеры

1. Алгоритм вычисления разности унарных чисел N, M. На вход подаётся строка N*M, где N и M — унарные числа в алфавите 1.
   1 * 1 → *
   * → .

2. Алгоритм поиска наибольшего общего делителя чисел N*M. Пусть a, b, c – служебные символы.
   1 a → a 1
   1 * 1 → a *
   1 * → * b
   b → 1
   a → c
   c → 1
   * → .

Визуализатор: http://cmcmsu.info/1course/alg.schema.nam.htm

Рефал

— [РЕкурсивных Функций АЛгоритмический] язык программирования, построенный на основе модели нормальных алгорифмов Маркова.

Функции задаются в терминах правил переписывания входных строк (деревьев) в выходные. Последовательность правил, разделённых символом ;. Слева от знака = записываются образцы, справа — результаты. После унификации входной строки с образцом выполняется подстановка полученных значений переменных в результат. Вызов функции — в угловых скобках, круглые скобки позволяют задавать и сопоставлять деревья и образцы на деревьях.

Для наглядности знак = заменён на →

Beta {
   (λ s.var '.'  e.body) t.value e.rest →
      Step <Subst s.var t.value e.body> e.rest ;
    → Stuck;
}

Турчин В. Ф. «Метаалгоритмический язык». Кибернетика, вып. 4 (1968 г.): 45–54.

Рефал

В образцах можно задавать переменные:

• s.имя-переменной принимает любой символ, не являющийся скобкой
• t.имя-переменной (терм) принимает любой символ, или парные скобки с их содержимым
• e.имя-переменной выполняет поиск. На первом шаге e-переменная пуста. Если не удалось сопоставить образец, e-переменная расширяется на следующий терм.

При успешном сопоставлении с образцом, значения переменных можно использовать при генерации результата.

Beta {
   (λ s.var '.'  e.body) t.value e.rest →
      Step <Subst s.var t.value e.body> e.rest ;
    → Stuck;
}

Н.М. Нагорный: алгорифмы Маркова можно эквивалентным образом задавать в виде нескольких конечных наборов правил подстановок [«функций»], бесконечного количества [функций] и бесконечного набора бесконечных функций.

Расширения Базового Рефала

Условия: промежуточный результат сопоставляется с образцом (Рефал-5):

t.neutral e.rest,
  <Beta e.rest> : s.state e.result =
  s.state t.neutral e.result ;

Функции высшего порядка: функции передаются так же, как и данные (Рефал-7):

(e.1) e.rest,
  <Beta e.1> : e.betaResult =
  <{
    Step e.result = Step (e.result) e.rest ;
    Stuck e.result,
      <Beta e.rest> : s.state e.result2 =
      s.state (e.result) e.result2 ;
  } e.betaResult>;

Рефал-5: В.Ф. Турчин. «Рефал-5. Руководство по программированию и справочник» http://refal.net/rf5_frm.htm
Рефал-7: С.Ю. Скоробогатов, А. М. Чеповский. «Разработка нового диалекта языка Refal». Информационные технологии, вып. 9 (2006 г.): 31–38.

Реализации языка Рефал

1. Интерпретатор Рефал-2 https://github.com/cmc-msu-ai/refal

2. Компилятор Рефал-7 в C (с поддержкой функций высшего порядка)

https://github.com/rfatkullin/bmstu-refal-compiler

https://github.com/rfatkullin/bmstu-refal-runtime

Метавычисления и суперкомпиляция

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

Суперкомпиляция — техника преобразования программ [в первую очередь — оптимизации], основанная на построении полной и самодостаточной модели программы.²

Две основные стадии суперкомпиляции:

1. Прогонка программы на параметризованных входных данных (частичная специализация). Выполняется построение множества конфигураций машины; в общем случае — в форме ориентированного графа с циклами.
2. Свёртка результата прогонки для получения конечной остаточной программы (выделение рекурсии).

¹ С.М. Абрамов. Основы метавычислений. Курс НОУ ИНТУИТ. http://www.intuit.ru/studies/courses/1067/221/info

² И.Г. Ключников. Суперкомпиляция: идеи и методы. Практика функционального программирования, № 7, 2011.

Примеры суперкомпиляции

Можно посмотреть здесь (для функционального языка программирования): http://spsc.appspot.com/all

Классический пример: суперкомпиляция наивного поиска постоянного образца P в строке S сложностью O(|P||S|) в поиск по алгоритму Кнута-Морриса-Пратта (KMP) сложностью O(|S|): http://spsc.appspot.com/view?key=agpzfnNwc2MtaHJkcjQLEgZBdXRob3IiGmlseWEua2x5dWNobmlrb3ZAZ21haWwuY29tDAsSB1Byb2dyYW0YzwEM

(для лучшего понимания: пример использования на практике близкой идеи ручной оптимизации сопоставления строки с набором образцов в конечный автомат на языке C: http://craftinginterpreters.com/scanning-on-demand.html#identifiers-and-keywords)

(и где-то натыкался около года назад на заметку об аналогичной оптимизации в компиляторе C/C++, но не нашёл)

Более простой пример: упрощение преобразования дерева в список: http://spsc.appspot.com/view?key=agpzfnNwc2MtaHJkcjULEgZBdXRob3IiG2pvaG5pY2hvbGFzQGpvaG5pY2hvbGFzLmNvbQwLEgdQcm9ncmFtGOkHDA

(Нетипизированное) λ-исчисление Чёрча (1932)

— изначально было предложено в качестве формальной системы для оснований математики.

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

Пример: f(x) = (x + 3)/x в «λ-исчислении»:

λx.(x + 3)/x — функция от аргумента x, значение которой равно (x + 3)/x.

Вызов f(2):

(λx.(x + 3)/x) · 2 — подставить 2 вместо x в выражение (x + 3)/x:

(λx.(x + 3)/x) · 2 ⟶ (2 + 3)/x ⟶ (2 + 3)/2

Строгое определение

Рассмотрим формулы, составленные из выражений вида:

1. x, y, z, … — переменная
2. λx.F — абстракция (x — имя переменной, которая может встречаться в формуле F)
3. A · B — приложение (применение, аппликация), A, B — формулы. Оператор «·» левоассоциативен (A · B · C = (A · B) · C).

Правило подстановки (β-редукция): (λx.F) · G⟶_βF[x := G]

Буква α зарезервирована для понятия α-эквивалентности — формулы, эквивалентные с точностью до переименования переменных:

λx.x=_αλy.y

Переменная, перед которой стоит соответствующая абстракция называется связанной, в противном случае — свободной:

λx.x · y — x связана, y свободна.

Вычисление считается завершённым когда нет β-редексов (подформул, к которым применима β-редукция)

Примеры

1. Нумералы Чёрча — представляем натуральное число n как n-кратное применение функции:

0 ≡ λf.λx.x

1 ≡ λf.λx.f · x

2 ≡ λf.λx.f · (f · x)

...

2. Композиция функций: f ∘ g ≡ g(f(x)) ≡ λf.λg.λx.g · (f · x)

3. Ω ≡ (λx.x · x) · (λx.x · x) — редукция этого терма уходит в бесконечный цикл.

Онлайн-интерпретаторы:

• https://jacksongl.github.io/files/demo/lambda/index.htm#firstPage
• https://projectultimatum.org/cgi-bin/lambda?t=(%CE%BBf.%CE%BBx.f%20(f%20x))%20(%CE%BBf.%CE%BBx.f%20(f%20x))%20(%CE%BBx.x)%20(%CE%BBx.x)&r=[LL(Beta)]&m=any%20order
• https://www.cl.cam.ac.uk/~rmk35/lambda_calculus/lambda_calculus.html

Свойства нетипизированного λ-исчисления

Теорема Чёрча-Россера

β-редукция конфлюэнтна.

Правила редукции можно применять в разном порядке (λ x . f · (g · x))

Формулировка: если x⟶^*y и x⟶^*z с помощью разной последовательности применения правил редукции, то существует терм w, для которого y⟶^*w и z⟶^*w.

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

«свойство ромба»

Схема доказательства теоремы Чёрча-Россера

(Tait, Takahashi; Komori, Matsuda, Yamakawa)

https://dx.doi.org/10.1007/s11225-013-9470-y

1. Takahashi translation for β-reduction: term M ↦M* (однократное параллельное применение β-редукции везде, где это возможно):

1. x* ≡ x
2. ((λx. M₁) · M₂)* ≡ M₁* [x := M₂*]
3. (M₁ · M₂)* ≡ M₁* M₂*
4. (λ x. M)* ≡ λ x. M*

Здесь и далее правила считаются упорядоченными: если можно применить несколько правил, применяется правило с наименьшим номером.

Индуктивно определим n-кратное применение: Mⁿ*.

Далее используем обозначения:

• →ᵦ₁ однократная β-редукция;
• →ᵦₙ n-кратная β-редукция;
• →ᵦ транзитивное замыкание β-редукции

Схема доказательства теоремы Чёрча-Россера

2. Свойства M* (леммы):

1. FV(M*) ⊆ FV(M)
2. M →ᵦ M*
3. M →ᵦ₁ N ⇒ N →ᵦ M*
4. ((λx.M) N)* β→ (M [x:=N])*
5. M →ᵦ₁ N ⇒ M* →ᵦ N*
6. M →ᵦ N ⇒ M* →ᵦ N*
7. M →ᵦ N ⇒ Mⁿ* →ᵦ Nⁿ*

3. Теорема 1. M →ᵦₙ N ⇒ N →ᵦ Mⁿ*

4. Теорема 2 (Чёрча-Россера). Если M →ᵦ M₁ и M →ᵦ M₂, то существует такой терм N, что:

M₁ →ᵦ N и M₂ →ᵦ N

Нормализация

Редекс — терм удаления, к которому можно применить правило редукции.

Нормальная форма терма относительно редукции — это такой вид, при котором к нему неприменимы правила редукции.

Головная нормальная форма терма — если в головной позиции (корне дерева) не стоит редекс.

Нормализация — свойство формальной системы: если у терма есть нормальная форма, то она единственная.

Сильная нормализация — у всех термов есть единственная нормальная форма (= нет термов, редукция которых не завершается).

Комбинаторная логика

M. Schönfinkel (1924), H. Curry (1930) Формальная система, синтаксис которой состоит из переменных, парных скобок и комбинаторов (правил преобразования строк символов). Эквивалентна машине Тьюринга, близко связана с λ-исчислением (может считаться «синтаксическим сахаром» для λ-исчисления)

• S x y z = x z (y z) — распределение
• K x y = x — отмена
• (S, K — базис, из них можно получить остальные комбинаторы)
• I x = x — идентичность
• D x = x x — дублирование
• C x y z = x z y — перестановка
• B x y z = x (y z) — композиция
• W x y = x y y — копирование
• Y x = x (Y x) — неподвижная точка

Y-комбинатор

Y-комбинатор — примитивный комбинатор рекурсии. Принимает на вход функцию двух аргументов, первый из которых — «рекурсивный вызов», а второй — входные данные для функции:

Y = λf.(λx.f(x · x)) · (λx.f(x · x)).

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

Fact := Y (λ fact. λ x.
    if (x == 0) return 1
    else return x*fact(x - 1))

Yx = x · (Yx)

«Тип» Y-комбинатора: ((T → T) → T → T) → T → T.

Парадокс Карри

1935 (Клини, Россер), 1941 (Карри), 1942 (Карри) Если дана формальная система, удовлетворяющая следующим свойствам:

• конечное число примитивных термов, единственная операция — бинарная операция применения, единственный унарный предикат — предикат выводимости «⊦ A»

• определено равенство в терминах примитивного терма Q и применения (X = Y ≡ ⊦ Q · X · Y)

• равенство симметрично, транзитивно, сохраняется при применении и подразумевает взаимную выводимость (A = B, A ⊦ B)

• для любого терма M со свободными переменными X₁, …, X_n существует терм M^*, такой, что M^* · X₁ · … · X_n = M

• может быть определён оператор импликации →, такой, что для любых термов M, N:

  • ⊦ M → M
  • ⊦ (M → (M → N)) → (M → N)
  • ⊦ M и ⊦ M → N ⟹ ⊦ N ...

Парадокс Карри

...[Если дана формальная система, удовлетворяющая свойствам на предыдущем слайде,]
то любой терм ξ выводим с помощью следующего построения:

1. Положим φ ≡ Y (λ x . x → (x → ξ))
2. ⊦ φ = (φ → (φ → ξ)) по определению Y
3. ⊦ φ = (φ → (φ → ξ)) → (φ → ξ) по определению Y
4. п. 3 — аксиома импликации, поэтому ⊦ (φ → (φ → ξ)) → (φ → ξ)
5. φ → (φ → ξ) (подставляем равенство из шага 2)
6. ⊦ φ Опять подставляем равенство из шага 2
7. По MP получаем φ → ξ и наконец ξ.

Основная идея — если формальная система допускает неограниченный оператор рекурсии (неподвижной точки), то она противоречива. Это справедливо для любой формальной системы, эквивалентной комбинаторной логике или λ-исчислению.

Principia Mathematica

B. Russel, A. Whitehead. 1910 – 1913 (3 тома). — фундаментальный труд по формализованным основаниям математики.

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

Для того, чтобы преодолеть парадокс Рассела, предлагалось рассматривать объекты как принадлежащие к некоторым типам. Типы определяются как область истинности некоторого утверждения.

λ-исчисление с простыми типами

1940 (Чёрч); далее представлено определение ближе к современной записи.

http://plato.stanford.edu/entries/type-theory-church/

Пусть дано множество базовых типов B, * ∈ B

Допустимые типы: τ ≡ b | τ₁ → τ₂,   b ∈ B.

Стрелка — правоассоциативна: α → β → γ ≡ α → (β → γ)

Сокращение: α' ≡ α → α

• * — «тип типов», тип высказываний

• У Чёрча — в обратном порядке и без стрелок (α → β → γ ≡ (γβα))

(тоже логичная запись: γβα · α, α взаимно-уничтожаются, остаёся γβ)

λ-исчисление с простыми типами

В оригинальной формулировке формулы:

• Символы λ, [, ] для описания абстракции
• Переменные a_α, b_α, … типа α
• Логические константы :
  • ¬_{*  → *} отрицание
  • ∨_{*  →  *  → *} дизъюнкция,
  • Π_{(α →  * ) → *} универсальная квантификация,
  • i_{(α →  * ) → α} оператор выбора
• Константы произвольных типов α

λ-исчисление с простыми типами

Современная формулировка исчисления (только вычислительная часть) не содержит логических констант и типа * (точнее, * — это «тип всех типов», но не входит в константу τ)

Грамматика:

• Абстракция (записывается как λx_α[A_α])
• Применение
• Константы и переменные

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

Естественная дедукция

τ ≡ b | α → β

Правила типизации, используемые для определения типов, можно структурировать (следующая структура носит название «естественная дедукция», natural deduction):

формация (Formation) — как определяется конструктор типа

α, β—типы ⟹ α → β—тип

введение (Introduction) — как определяются элементы типа

Γ, x : σ ⊦ e : τ ⟹ λx_σ.e : σ → τ

удаление (Elimination) — что можно делать с элементами типа, чтобы получить элементы некоторого другого типа

Γ ⊦ x : σ → τ, Γ ⊦ y : σ ⟹ Γ ⊦ x_{σ → τ} · y_σ : τ, x — удаляемый терм

редукция (Reduction) — взаимное уничтожение термов введения и удаления (не входит в обычное понятие естественной дедукции)

[λx.F] · G⟶_βF[G/x]

Безопасность типов

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

1. Определим множество «канонических» (простых) форм для типов. Каноническая форма — это значение, записанное в явном виде:

• 1 — это каноническая форма натурального числа;
• (λx_ℕ.x) · 1 — это не каноническая форма натурального числа;
• 1 · 1 — это некорректно типизированное выражение.

2. (Progress) Любой корректно типизированный терм t : T без свободных переменных или находится в канонической форме, или является редексом. Доказательство — по индукции вывода типа. Нетривиальный случай — применение T-App.

3. (Preservation) Редукция сохраняет тип, т.е. если t : T и t ⟶ t′, то t′ : T. Доказательство — по индукции по выводу типа. Для случая подстановки нужно доказать, что операция подстановки сохраняет типизацию. Для этого, в свою очередь, нужно показать, что типизация сохраняется при изменениях в контексте, которые не изменяют значения свободных переменных.

4. Безопасность типов: если вычисление любого корректно типизированного терма завершается, то результатом вычисления является каноническая форма.

Эквивалентность термов

Обычно определяется следующим образом: A эквивалентен B, если A и B приводятся β-редукцией к идентичному виду, с точностью до корректных (без конфликтов имён) переименований переменных. На индексах де Брёйна последнее замечание неактуально.

η-эквивалентность

Пусть f : α → β. Тогда λ(x : α).f · x интуитивно эквивалентен исходной f, но по указанному выше определению формально это разные термы.

η-эквивалентность включает такое понятие и, в случае просто типизированного λ-исчисления, не нарушает разрешимости эквивалентности типов.

Проверка типов разрешима — если есть алгоритм, который для любого терма определяет, корректно ли он типизирован. Эквивалентность термов разрешима — если есть алгоритм, который для любой пары термов определяет, эквивалентны ли они при заданных правилах.

Не все утверждения удобно представимы в λ-исчислении с простыми типами

В частности, для нумералов Чёрча представимый класс называется «расширенные полиномы» над ℕ:

• 0, 1, проекции
• сложение, умножение
• функция ifzero(n, m, p) = if n = 0 then m else p

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

Задачи

Задача 5.1. *

Определить умножение и сложение для нумералов Чёрча.

Задача 5.2. **

Показать, что, хотя для некоторого базового типа T нумералы Чёрча и их умножение и сложение типизируемо, нельзя определить операцию вычитания нумералов в λ-исчислении с простыми типами.

Задача 5.3а. **

Построить машину Тьюринга, которая делает β-редукцию.

Задача 5.3б. **

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

Задача 5.4а. **

Построить нормальный алгорифм Маркова, который делает β-редукцию.

Задача 5.4б. **

Написать пошаговый эмулятор β-редукции на языке Рефал.