«Знаменитые логики допустили здесь неловкие ошибки», - говорится в сообщении SICP. К чему это относится?

Вот контекст ( Структура и интерпретация компьютерных программ , раздел 1.1.8, под заголовком «Локальные имена»):

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

В конце этой последней строки есть сноска (26), которая гласит:

Концепция последовательного переименования на самом деле тонкая и ее трудно определить формально. Знаменитые логики допустили здесь неловкие ошибки.

На что или на кого ссылается текст? Почему определение «согласованного переименования» было бы трудным, какие логики допустили ошибки, пытаясь определить это, и что это были за ошибки?

logic ubadub
источник

Я говорю своим ученикам, что единственный способ понять «последовательно переименовывать связанные переменные» - правильно реализовать эту чертову вещь. Многие книги по логике избегают этой проблемы, дают неполные процедуры переименования или, по крайней мере, пропускают доказательства того, что данные процедуры переименования верны. Но я не знаю, к каким конкретно сплетням относится книга.

Андрей Бауэр

Точная работа с переименованием переменных, новыми именами, заменой без захвата и тому подобным - одна из самых тривиальных вещей, которая быстро становится действительно громоздкой в определениях и доказательствах. Для такой тривиальной проблемы человек не хочет тратить больше, чем тривиальное количество умственных циклов, но гораздо больше, чем это потребуется, чтобы избежать многих хитрых захватов / столкновений / и т. Д. Часто люди ЛП проявляют некоторую осторожность в своих определения, но затем вызвать "конвенцию Барендрегта" и игнорировать проблему, несколько злоупотребляя "свежим" здесь и там, когда это необходимо.

Чи

Буду признателен за более конкретные ответы, ниже, в поле для ответов, если это вообще возможно. Эти комментарии все еще заставляют проблему звучать загадочно, поскольку вы написали их для чтения кем-то, кто уже знаком с этой проблемой, в то время как я не

ubadub

@chi, в частности, я был бы признателен за чтение рекомендаций, касающихся этой темы, если они у вас есть. Заранее спасибо

убадуб

Это частичный ответ: я понятия не имею, о каких ошибках или людях ссылается SICP. Я могу лишь дать некоторые подсказки о том, «почему» переименование переменной может быть болезненным для точной обработки.

Прежде всего, это кажется тривиальным для определения. Например, мы можем переименовать связанные переменные в индексированных суммах

\sum_{x} e = \sum_{y} (e {y / x})

$\sum_x e = \sum_y (e\{y/x\})$

где $e$ - любое выражение, а $e\{y/x\}$ обозначает синтаксическую замену каждого $x$ на $y$ . Тривиально, правда?

Ну, если мы слепо применяем правило выше, мы получаем

\sum_{x} (x + y) = \sum_{y} (y + y)

$\sum_x (x+y) = \sum_y (y+y)$

Это не хорошо. Нам нужно добавить требование « $y$ не встречается в $e$ », или мы получим конфликт имен.

Теперь рассмотрим это правильное переименование

\sum_{x} \sum_{y} (x + y) = \sum_{x} \sum_{z} (x + z)

$\sum_x \sum_y (x+y) = \sum_x \sum_z (x+z)$

если мы хотим переименовать $x$ в $y$ , по вышеупомянутому правилу мы можем сделать это с правой стороны, но не с левой стороны. Это неудобно, поскольку они отличаются только переименованием, поэтому они должны обрабатываться одинаково.

Типичный подход здесь - прибегнуть к переопределению $e\{y/x\}$ как «замены, избегающей захвата», и ослабить требование » $y$ не встречается в $e$ » и использовать вместо него « $y$ не встречаетсясвободнов $e$ ».

Затем мы определяем бесплатные вхождения:

f r e e (x) = {x} f r e e (e + t) = f r e e (e) \cup f r e e (t) f r e e (\sum_{x} e) = f r e e (e) ∖ {x}

$free(x)=\{x\} \qquad free(e+t) = free(e)\cup free(t) \qquad free(\sum_x e) = free(e)\setminus\{x\}$

Наконец, захват, избегающий замены:

$x\{t/y\}$ является $t$ если $x=y$ , и $x$ противном случае.
$(e+e')\{t/y\} = e\{t/y\} + e'\{t/y\}$ (простой случай)
$(\sum_x e)\{t/y\} = ??$

Последний случай болезненный. Если $x=y$ , подстановка запрещена, так как мы хотим, чтобы она влияла только на свободные переменные, а $x$ связан. Таким образом, результат просто $\sum_x e$ .

Если $y\neq x$ , мы хотели бы сказать, что $(\sum_x e)\{t/y\} = \sum_x (e\{t/y\})$ . Это, однако, в общем случае неверно, так как если $x$ появляется свободным в $t$ мы получаем перехват.

Вздох. Итак, мы допустим, чтобы $z$ была «первой» переменной, которая 1) не $y$ , 2) не свободна в $t$ и 3) не свободна в $\sum_x e$ . Здесь «первый» означает, что нам нужно упорядочить набор имен переменных (например, выбрав биекцию между именами и натуральными числами). Затем, наконец, пусть $(\sum_x e)\{t/y\} = \sum_z (e\{z/x\}\{t/y\})$ .

Надеюсь, я понял это правильно. (Кстати, моя первая попытка была ошибочной)

$z$ $z$

$\alpha$ $\lambda x$

Теперь представьте, что приходится иметь дело с этим сложным определением каждый раз, когда мы хотим доказать что-то в теории PL. Мы могли бы, но мы не хотим. Это скучно, утомительно, подвержено ошибкам, загромождает доказательства и не дает читателю понимания. По этой причине многие авторы PL просто пропускают детали, говоря (или даже принимая как должное!), Что термины должны приниматься «вплоть до переименования переменных», что все связанные переменные предполагаются отличными от того, от чего они должны отличаться, что мы принимаем «конвенцию Барендрегта», или что-то в том же духе.

Честно говоря, это обман в доказательствах. Мы могли бы также добавить «подмигнуть, подтолкнуть, сказать больше!» в том же духе. По сути, мы просим пощады и говорим читателю: «Смотри, это скучно, я не хочу это делать, ты не хочешь читать это - мы оба знаем, что, приложив огромные усилия, мы могли бы переписать это доказательство, чтобы включить все детали ".

Технически это это можно использовать этот ярлык , чтобы доказать ложное утверждение. Опытный рецензент, однако, знает, что "морально хорошо" и что можно сделать идеальным (с большими усилиями), а что подозрительно. Последнее может включать в себя что-то, что зависит от фактического выбора связанных имен (поэтому мы не работаем "до", как обещали!). В этих случаях рецензия запросит более подробную информацию, чтобы его можно было убедить.

чи
источник

«Знаменитые логики допустили здесь неловкие ошибки», - говорится в сообщении SICP. К чему это относится?

Ответы: