Представяне на термини без използване на имена

В предишната глава работихме с термините>. Съгласихме се, че свързаните променливи могат да бъдат преименувани по всяко време, за да се извърши заместване или ако новото име е по-удобно по някаква причина. По принцип, свързаното име на променлива може да бъде всичко. Тази конвенция работи отлично, когато се обсъждат основните идеи на ламбда смятането и ви помага да записвате ясно доказателства. Когато обаче прилагаме смятане в програма, трябва да имаме едно представяне за всеки член; по-специално, трябва да решите как ще бъдат представени променливите записи. Има няколко начина за решаване на този проблем: 1

Възможно е да се представят променливи символично, както правехме досега, но вместо неявно преименуване, ние изрично заместваме свързаните променливи> с имена, когато е необходимо заместване, за да се избегне улавянето.
Можете да представите променливите символично, но изисквате имената на всички обвързани променливи да се различават едно от друго и от всички свободни променливи, намерени другаде. Такова споразумение (понякога наричано Barendregt конвенция) е по-строго от нашето, тъй като не позволява да се преименуват променливи> в произволно време. Това правило обаче не е безопасно по отношение на заместването (или бета редукцията): тъй като заместеният термин се копира, не е трудно да се конструират примери, при които заместването води до термин, в който няколко λ-абстракции имат едно и също име на променлива на свързване . Следователно, след всяка стъпка на изчисление, която включва заместване, трябва да последва стъпка за преименуване, възстановяваща инварианта.
Можете да изградите> представяне на променливи и термини, в които не е необходимо преименуване.
Можете изцяло да избегнете идеята за заместване, като използвате механизми като изрични замествания (Abadi, Cardelli, Curien и Lévy, 1991a).
Използването на променливи може да бъде избегнато чрез работа на език, базиран на комбинатори, например комбинаторна логика (Curry and Feys, 1958, Barendregt, 1984), вариант на ламбда смятане, който използва комбинатори вместо процедурна абстракция. - или в език на Backus FP (Backus, 1978).

Всяка от тези схеми има своите поддръжници и изборът между тях е донякъде въпрос на вкус (при сериозни изпълнения на компилатор съображенията за производителност също трябва да бъдат взети под внимание, но сега не ни пука за тях). Избираме третия вариант, който според нашия опит ще се мащабира по-добре, когато трябва да работим с някои от по-сложните преводачи в тази книга. Неговото предимство е, че в случай на грешки при изпълнението, алгоритъмът веднага дава очевидно грешни резултати в най-простите случаи. Това ви позволява бързо да откривате и коригирате грешки. Напротив, има случаи, когато при реализации, базирани на именувани променливи, грешки са били откривани след месеци и години. Нашата реализация използва добре познатия метод, изобретен от Николас де Браун (de Bruijn, 1972).