Машины Тьюринга и эквивалентность лямбда-исчисления

Проще говоря, вы просто доказываете две вещи:

1. Для любого лямбда-члена существует машина Тьюринга, которая вычисляет то же самое.
2. Для любой машины Тьюринга есть лямбда-член, который вычисляет то же самое.

Конечно, здесь есть некоторая махинация, так как вам также необходимо учитывать операционные различия в вводе/выводе, но мы не будем вдаваться в это здесь.

На практике две приведенные выше теоремы доказываются конструктивно, т. е. фактически давая механический способ превращения одной в другую. Таким образом, вы предоставляете два компилятора вместе с доказательством их правильности.

Чтобы получить хорошую интуицию, подумайте об аналогичной теореме эквивалентности между лямбда-исчислением и регистровыми машинами. В этих условиях, отмахиваясь от конечности реального компьютера, интерпретатор нетипизированного лямбда-исчисления является доказательством в одном направлении. И здесь я имею в виду реальную, осязаемую программу, которую вы можете запустить; например удалив средство проверки типов из компилятора функционального языка программирования (в который обязательно должна быть встроена какая-то типизированная версия лямбда-исчисления.

Так что в следующий раз, когда будете запускать GHC, подумайте об этой теореме!

Я считаю, что логика ворот (аппаратное обеспечение), лямбда-исчисление (математика/абстракция) и машины Тьюринга (абстрактные изображения) — это одна и та же операция с другой точки зрения. Gate Logic — это биты/ток, которые сдвигаются. Вы можете реализовать его самостоятельно вручную (экспериментальные наборы, макет, аппаратное обеспечение) или использовать симулятор логического элемента (программное обеспечение) для тестирования. Лямбда-исчисление — это формальная и математическая концепция, доказывающая, что операция, которую вы выполняете механически, всегда будет иметь один и тот же вывод/результат. Машины Тьюринга — это просто более абстрактный способ объяснить это, без математики и Гейтса. Расскажите своей бабушке об архитектуре фон Неймана, оставив математику, электротехнику и разработку программного обеспечения в лаборатории. В логике вентилей вы создадите защелку, которая будет удерживать бит/состояние в зависимости от входных данных. В лямбда-исчислении каждый бит является символом, а сама лямбда является символом перехода/редукции. В машинах Тьюринга биты — это регистры. Я научился этому с помощью Principia Mathematica, Tractatus-Logico Philosophicus и лямбда-исчисления: самые короткие объяснения являются худшими, потому что они самые абстрактные. Вам понадобится время, чтобы посмотреть на деревья, чтобы они стали лесом.