SMC-машина

Конфигурация

Управляющий стек

Стек (промежуточных и конечных) результатов

Память состояний

- частичная функция, отображающая адреса на целые числа, определенная только на конечном множестве адресов.

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

Определим начальные конфигурации в форме , где - команда ПЯК, а - состояние. Определим также конечные конфигурации как . Выполнение ПЯК-программы на SMC-машине описывается выражением , которое означает, что успешное выполнение команды в состоянии влечет переводит SMC-машине в состояние .