Решение функциональных уравнений для неизвестных функций в лямбда-исчислении

14

Существуют ли методы решения функциональных уравнений для неизвестных функций в лямбда-исчислении?

Предположим, у меня есть функция тождества, определенная как таковая:

Ix=x

(то есть, записывая уравнение для ожидаемого поведения этой функции) , и теперь я хочу , чтобы решить эту проблему для I , делая некоторое алгебраическое преобразование , чтобы получить интенсиональную формулу для этой функции:

I=λx.x

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

Конечно, функция тождества используется только в качестве примера. Меня интересуют более общие методы решения таких уравнений. В частности, я хотел бы найти функцию которая удовлетворяет следующему требованию:B

Bf(λx.M)=(λx.fM)

то есть «вводит» заданную функцию в заданную лямбда-функцию ( λ x . M ) перед ее «телом» M (которое является произвольным лямбда-выражением), возможно, разбирая ее и конструируя новую, чтобы она стал параметром, к которому применяется функция f .f(λx.M)Mf

BarbaraKwarc
источник

Ответы:

13

Это известная проблема, известная как Объединение высшего порядка .

К сожалению, эта проблема вообще неразрешима. Существует разрешимый фрагмент, известный как фрагмент шаблона Миллера. Он широко используется, в частности, при проверке типов программ с зависимой типизацией с метапеременными или сопоставлении с образцом. В этом фрагменте переменные объединения применяются только к различным связанным программным переменным.

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

К сожалению, не похоже, что ваша функция попадает в этот фрагмент шаблона. Тем не менее, то, что я вижу, очень похоже на композицию функций. Следующая функция удовлетворяет вашей собственности?

B=λf g x .f (g x)

У нас есть:

  • B f (λx.M)
  • по α -эквивалентности=B f (λy.[y/x]M)α
  • =λx.f ((λy.[y/x]M)x)
  • =λx.f ([x/y][y/x]M)
  • =λx.f M
jmite
источник
1
Да, похоже на это :) Забавно то, что я почти получил это решение, но по какой-то причине я подумал, что вызов чего-то «выполнит», испортив выражение: q То, что я пропустил что мы можем заменить переменную другой переменной, связанной снаружи. (λx.M)
BarbaraKwarc
1
Спасибо за ссылку на статью, я проверю ее и через пару дней приму ваш ответ, чтобы дать шанс другим людям.
BarbaraKwarc
3
Это объединение высшего порядка? Похоже, что вопрос не в типизированном лямбда-исчислении, а в простейшем лямбда-исчислении.
Питер Тейлор
2

Я думаю, что у меня есть частичный ответ относительно уравнения с тождественной функцией:

Ix=x

Мы хотим решить ее, найдя формулу для , которая будет иметь форму ( λ p . M ) с некоторым еще неизвестным выражением M в качестве тела. Давайте заменим это на I в исходном уравнении:I(λp.M)MI

(λp.M)x=x

затем примените функцию к с левой стороны:x

M[p/x]=x

Но что у нас здесь? :> Это уравнение является формулой для выражения мы ищем, после замены каждого вхождения p в нем на x , и оно говорит, что оно должно выглядеть как правая часть впоследствии :) Другими словами, функция, которую мы искал это:Mpx

I=(λx.x)

что, конечно, правильный ответ :)


ω

ωω=ωω

ω(λx.M)M

(λx.M)ω=ωω

M

M[x/ω]=ωω

xMωωωMxx

ω=(λx.xx)

это действительно так :)


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

BarbaraKwarc
источник
M[x/ω]=ωωω=(λx.xx)
В этих двух простых случаях - да, есть: просто обратная замена. Но, как я уже сказал, эти случаи могут сработать по чистой случайности: правая часть уже находится в требуемой форме. Когда я попробовал это на более сложных примерах, это не сработало. Это то, что я ищу, хотя: для алгоритмического пути.
BarbaraKwarc
1
ωω=ωωωω