SECD-машина — абстрактная машина, интерпретатор выражений λ-исчисления. Использует четыре стека: S (англ. stack) — стек объектов для вычисления рекурсивных выражений, E (англ. environment) — контекст (отображение идентификаторов в объекты), C (англ. control list) — управляющая строка (список управления), D (англ. dump) — дамп, хранилище предыдущих состояний, используемое для возврата из вызова функций.
Интерпретатор предложен в 1964 году Питером Лэндином в статье «The Mechanical Evaluation of Expressions» (механическое вычисление выражений)[1]. SECD-машина легла в основу многих практических реализаций функциональных языков программирования (как энергичных, так и ленивых вычислений), хотя и требует оптимизации.[2]
В любой момент SECD-машина имеет состояние, представленное в виде кортежа из четырёх стеках, а её работу можно описать с помощью функции перехода из одного состояния в другое.
В самом начале контекст E, стек S и дамп D пусты, а подлежащее вычислению выражение загружается как единственный элемент C, который преобразуется в обратную польскую нотацию в процессе вычислений. Единственной используемой при этом операцией является аппликация, обозначаемая символом ap (от англ. apply — применить). Например, выражение f (g x) (единственный элемент списка) заменяется списком [x, g, ap, F, ap].
Вычисление C выполняется в соответствии с обратной польской логикой. Если первый элемент в C является значением, он помещается на стек S. Точнее, если элемент является идентификатором, значение будет привязкой для этого идентификатора в текущем контексте E. Если элемент является λ-абстракцией, для сохранения привязок его свободных переменных (которые находятся в E) формируется замыкание, которое помещается в стек S.
Если элементом С является ap (аппликация), из стека извлекаются два значения, и первое применяется ко второму. Если результатом аппликации является значение, оно помещается в стек S.