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

Question

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

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

Answer 1

Вот пример:

\f -> f x 

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

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

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

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

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

Answer 2

Ну, here's the relevant Wikipedia article, для чего это стоит.

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

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

Eta reduction - это удаление лишнего слоя привязки и немедленное применение переменной, которая, как вы могли бы себе представить, действительна только в том случае, если рассматриваемая переменная используется только в одном месте.