Существуют ли методы решения функциональных уравнений для неизвестных функций в лямбда-исчислении?
Предположим, у меня есть функция тождества, определенная как таковая:
(то есть, записывая уравнение для ожидаемого поведения этой функции) , и теперь я хочу , чтобы решить эту проблему для , делая некоторое алгебраическое преобразование , чтобы получить интенсиональную формулу для этой функции:
это говорит о том, как именно функция выполняет ожидаемое (то есть, как реализовать ее в лямбда-исчислении).
Конечно, функция тождества используется только в качестве примера. Меня интересуют более общие методы решения таких уравнений. В частности, я хотел бы найти функцию которая удовлетворяет следующему требованию:
то есть «вводит» заданную функцию в заданную лямбда-функцию ( λ x . M ) перед ее «телом» M (которое является произвольным лямбда-выражением), возможно, разбирая ее и конструируя новую, чтобы она стал параметром, к которому применяется функция f .
источник
Я думаю, что у меня есть частичный ответ относительно уравнения с тождественной функцией:
Мы хотим решить ее, найдя формулу для , которая будет иметь форму ( λ p . M ) с некоторым еще неизвестным выражением M в качестве тела. Давайте заменим это на I в исходном уравнении:I (λp.M) M I
затем примените функцию к с левой стороны:x
Но что у нас здесь? :> Это уравнение является формулой для выражения мы ищем, после замены каждого вхождения p в нем на x , и оно говорит, что оно должно выглядеть как правая часть впоследствии :) Другими словами, функция, которую мы искал это:M p x
что, конечно, правильный ответ :)
это действительно так :)
Однако у меня есть ощущение, что это может быть так просто, потому что правая сторона уже была в той форме, которую мы ищем.
источник