Menu
Suppose that you want to find a λ-calculus program, T, that satisfies the following equations:
(T (λ f x . x)) = (λ a t . a)
(T (λ f x . (f x))) = (λ a t . (t a))
(T (λ f x . (f (f x)))) = (λ a b t . (t a b))
(T (λ f x . (f (f (f x)))) = (λ a b c t . (t a b c))
On this case, I've manually found this solution:
T = (λ t . (t (λ b c d . (b (λ e . (c e d)))) (λ b . b) (λ b . b)))
Is there any strategy for solving such λ-calculus equations automatically? What is the state of art on that subject?
871
Each functional equation provides some information about a function or about multiple functions. For example, f ( x ) − f ( y ) = x − y f(x)-f(y)=x-y f(x)−f(y)=x−y is a functional equation.
Functional equations are useful to understand the "symmetries" of a given function, pretty much as periodicity. For example, they may be used in the continuation of functions to the complex plane.
In mathematics, a functional equation is, in the broadest meaning, an equation in which one or several functions appear as unknowns. So, differential equations and integral equations are functional equations.
All the functions that satisfy a particular functional equation are known as solutions to that functional equation. It is hard to find solutions to functional equations. That is because there can be multiple (weird) functions satisfying the given conditions.
I'm not sure about state of the art, but William E Byrd's work on relational interpreters (such as this paper) allows program synthesis of this kind.
Also see his PolyConf talk for some neat stuff on searching for program terms. Your examples seem like they would be fairly easy to express in that way.
163
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
