Что такое "свободная переменная"?

(Я уверен, что на этом сайте уже был дан ответ, но поиск наводнен концепцией вызова free() для переменной в C.)

Я натолкнулся на термин "eta reduction", который был определен как f x = M x ==> M, если x "не является свободным в M". Я имею в виду, я думаю, что я понимаю суть того, что он пытается сказать, похоже, что вы делаете, когда вы конвертируете функцию в бесшумный стиль, но я не знаю, что означает квалификатор о том, что x не является бесплатным.

Ответы

Ответ 1

Вот пример:

\f -> f x

В этой лямбде x - свободная переменная. В принципе, свободная переменная - это переменная, используемая в лямбда, которая не является одним из аргументов лямбда (или переменной let). Это происходит вне контекста лямбда.

Это означает, что мы можем изменить:

(\x -> g x) to (g)

Но только если x не является свободным (т.е. не используется или является аргументом) в g. В противном случае мы создадим выражение, которое ссылается на неизвестную переменную:

(\x -> (x+) x) to (x+) ???

Ответ 2

Хорошо, вот соответствующая статья Википедии, для чего это стоит.

Краткая версия заключается в том, что такие определения верят в тело выражения лямбда с использованием заполнителя, такого как "M", и поэтому должны дополнительно указать, что переменная, привязанная этой лямбда, не используется в том, что представляет собой заполнитель.

Таким образом, "свободная переменная" здесь примерно означает переменную, определенную в некоторой двусмысленной или неизвестной внешней области - например, в выражении типа \y -> x + y, x является свободной переменной, но y не является.

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