А-машина Тьюринга и кофе-машина Хоара пит-стоп
В Священных Языковых Войнах в качестве окончательного аргумента нередко приводят — поскольку языки полны по Тьюрингу, постольку они и равноценны. Под катом попытка уточнить этот тезис для тех, кто уже справился с Python и теперь планирует изучить Erlang или Haskell по спецификации. Материал обзорный, не методичный с картинками.
Алан Тьюринг построил свою а-машину в 1936 году.
1948 essay, «Intelligent Machinery» Turing.
Можно сказать, что внутри машины припрятан конечный автомат, так будет понятней практикам. Конструктор из которого можно собрать любую а-машину считается полным по Тьюрингу. Две машины считаются эквивалентными по Тьюрингу если из деталек одной можно собрать другую. Тьюринг прототипировал универсальный агрегат, способный заменить произвольную а-машину. Универсальная Машина Тьюринга добивается такого, просто считывая с ленты вместе с данными описание какой нибудь частной а-машины. Любые две УМТ очевидно эквивалентны. И в 1946 году фон Нейман этот прототип построил. Здесь стоит отметить, что УМТ логарифмически медлительней частной а-машины на сложных вычислениях. Тьюринг с Черчем постулировали: любая функция натуральных чисел вычислима человеком снабженным бумагой и карандашом тогда и только тогда, когда с ней справится Универсальная Машина Тьюринга. Из вышесказанного вытекает — круче Универсальной Машины Тьюринга ничего и быть не может. Что ни строй, все равно УМТ получится (если тезис Черча-Тьюринга верен). Все же Тьюринг вынужден был признать, что машина его без тормозов. Из за теоремы Геделя о неполноте возникает проблема останова. Нельзя быть уверенным, что УМТ всегда достигнет состояния Стоп. Вычисления в УМТ это последовательность шагов по ленте и смены состояний. К примеру модуль целого числа abs(int) на ассемблере можно взять так Императивные языки программирования имеющие if и goto реализуют Универсальную Машину Тьюринга.
В том же 1936 году Алонзо Черч представил миру лямбда исчисление описанное тремя немудреными правилами о своих термах. (Вообще исследования Черча датируются 1928-1930гг, а Тьюринг был аспирантом Черча и все же опубликованы работы были в одно время.) • Переменные x, y, z… являются термами.(Алфавит) • Если M и N – термы, то(MN)–терм.(Применение) • Если x–переменная, а M–терм, то(λx.M)–терм.(Абстракция) Ну и еще уточняется, что все остальное вообще не лямбда термы. Абстракция здесь — способ описать функцию. Применение — возможность применить ее к аргументам. Лямбда выражение может быть отлично представлено деревом.
- α-conversion: переименование аргумента (alpha); λx.x → λy.y
- β-reduction: применение функции к аргументам (beta); ((λn.n*2) 7) → 7*2
- η-conversion: подмена равнозначным (eta). λx.(f x) → f
Когда выражение не поддается редуцированию оно считается вычисленным и находящимся в нормальной форме. Вычисления — это последовательность упрощений. В 1958 году Джон МакКарти реализует лямбда исчисление в языке Lisp способном исполняться на машине фон Неймана. Lisp это реализация лямбда исчисления а не машины Тьюринга(в нем нет goto), но согласно тезису Черча-Тьюринга он такой машиной является. Начинающему практиковать Lisp следует первым делом осознать что последовательность действий программы на функциональном языке нам в общем случае неизвестна и не важна, как не важна очередность упрощений примененных вычислителем к лямбда выражению. Представление кода и данных в Lisp единообразно это — list определяемый тремя операциями
а стек может быть описан например так
Да, лямбда исчисление Тьюринг эквивалентно, но только не типизированное. Вводя ограничение типов термов мы хотя и обобщаем формализм но при этом умаляем общность понятия терм. Типизированное лямбда исчисление в общем случае не полно по Тьюрингу.
Что бы добиться полноты необходимы дополнительные абстракции. И в 1942-1945 годах Эйленберг с Маклейном создают такую абстракцию — теорию категорий. Черч называет теорию категорий
- ассоциативную: h ∘ (g ∘ f) = (h ∘ g) ∘ f
- и отождествляемую id : x → x id ∘ f = f = f ∘ id.
Функторы — это отображения категорий, сохраняющие структуру.
Натуральное преобразование — это отношение двух функторов.
В начале 1970х Гирард и Рейнольдс независимо формулируют Систему-F, как полиморфное лямбда исчисление(по большому счету они допустили в лямбда нотации квантор всеобщности). Хиндли и Милнер разработали для выведения типов алгоритм-W сложности О(1), то есть линейной от размера выражения(для этого потребовалось сделать нотацию префиксной). Милнер встраивает систему в язык ML и к 1990 она появляется в Haskell. Таким образом в Haskell в вашем распоряжении категория Hask содержащая объектами все типы данных и морфизмами все возможные функции. Концепция Haskell отражает идею математика Хаскелла Карри, писавшего, что
Вычисления в таком формализме — это скажем, вывод декларированной категории, а результат вычислений расценивается как побочный эффект доказательства. Например для экспоненты разложенной в степенной ряд
мы можем сказать
Алгоритм-W и еще изящный математический фокус — монада, как обобщение структурной рекурсии позволили реализовать категорию Hask на машинах фон Неймана. Haskell полон по Тьюрингу хотя бы потому что полон его type-checker реализующий алгоритм-W. Но следует понимать, что язык проектировался не как машина Тьюринга, в теории категорий просто отсутствует абстракция state, на которой построены конечные автоматы. На практике изучающему Haskell полезно привыкнуть рассуждать о типах переменных и морфизмах между ними, а не значениях (которые неизменны).
Машина фон Неймана — последовательный вычислитель, но машины научились связывать в сети. В 1985 году Чарльз Хоар публикует документ «Сообщающиеся последовательные процессы», в котором развивает новый формализм. Предисловие пишет Дейкстра. Объект описывается в алфавите событий в которые он вовлечен. Совокупность таких событий формируют процесс. Возьмем аппарат массового обслуживания
Пусть x это событие, а P это процесс, тогда: (произносится как «x затем P») описывает объект, который сначала совершает событие x, а затем ведёт себя как P. где X — локальная переменная, которая может быть изменена Последовательность событий пройденных объектом составляет трассу процесса. Окружение процесса рассматривается также как последовательный процесс. Два процесса могут иметь в алфавите одинаковые события Сладкоежка не прочь получить ириску бесплатно, но чудес не бывает
В такой нотации Хоар строит алгебру способную эффективно решать(по меньшей мере диагностировать) 'Проблему обедающих философов' и выводит законы этой алгебры.
Формализм реализован в Erlang, Golang, Ada библиотеках Haskell и других языков. Являются ли две машины Тьюринга посаженные на одну ленту машиной Тьюринга?
Да, отвечает Хоар. Он декларирует свою алгебру в термах лямбда исчисления и реализует на Lisp. Теперь принято соглашение, что взаимодействующие последовательные процессы всегда могут быть тривиально представлены одним запущенным на машине фон Неймана. Обратная задача, выделение в процессе двух взаимодействующих — отнюдь не тривиальна. Вот так может выглядеть конкурентное решето для первых десяти простых чисел на языке Go
С практической точки зрения программируя конкурентно на Erlang, Go или просто для web важно вначале определиться с общим алфавитом(разделяемыми ресурсами) процессов. Языки имеющие инструментарий для параллельного программирования провоцируют этот инструментарий использовать. Надо помнить при этом, что любой алгоритм может быть реализован последовательно и как правило эффективней.
Итак, да — описанные формализмы эквивалентны по Тьюрингу. Однако в подражение Тьюрингу доказывать это каждой программой путем реконструкции одной парадигмы в рамках другой кажется мне контрпродуктивным. Со своим уставом в чужой монастырь не ходят. Принимая на вооружение язык исповедующий фундаментально другую модель вычислений приходится пересматривать устойчивые навыки, метрики и паттерны проектирования.