patternModerate
Solving functional equations for unknown functions in lambda calculus
Viewed 0 times
solvingequationscalculusunknownforfunctionalfunctionslambda
Problem
Are there any techniques for solving functional equations for unknown functions in lambda calculus?
Suppose I have the identity function defined extensionally as such:
$I x = x$
(that is, by writing down an equation for the expected behaviour of that function) and now I want to solve it for $I$ by doing some algebraical transformation to get the intensional formula for that function:
$I = \lambda x.x$
that tells how exactly does the function do what was expected (that is, how to implement it in lambda calculus).
Of course the identity function is used just as an example. I'm interested in more general methods of solving such equations. In particular, I would like to find a function $B$ that satisfies the following requirement:
$B\;f\;(\lambda x.M) = (\lambda x.f M)$
that is, "injects" the given function $f$ into the given lambda function $(\lambda x.M)$ before its "body" $M$ (which is some arbitrary lambda expression), possibly by taking it apart and constructing a new one, so that it became a parameter the function $f$ is applied to.
Suppose I have the identity function defined extensionally as such:
$I x = x$
(that is, by writing down an equation for the expected behaviour of that function) and now I want to solve it for $I$ by doing some algebraical transformation to get the intensional formula for that function:
$I = \lambda x.x$
that tells how exactly does the function do what was expected (that is, how to implement it in lambda calculus).
Of course the identity function is used just as an example. I'm interested in more general methods of solving such equations. In particular, I would like to find a function $B$ that satisfies the following requirement:
$B\;f\;(\lambda x.M) = (\lambda x.f M)$
that is, "injects" the given function $f$ into the given lambda function $(\lambda x.M)$ before its "body" $M$ (which is some arbitrary lambda expression), possibly by taking it apart and constructing a new one, so that it became a parameter the function $f$ is applied to.
Solution
This is a known problem, known as Higher Order Unification.
Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used extensively in, among other things, typechecking of dependently-typed programs with metavariables or pattern matching. This fragment is where unification variables are applied only to distinct bound program variables.
This paper provides a great tutorial of how higher order unification works, and walks through a (relatively) simple implementation of it.
Unfortunately, it doesn't look like your function falls into this pattern fragment. That said, what I'm looking seeing is pretty similar to function composition. Does the following function satisfy your property?
$B = \lambda f\ g\ x\ \ldotp f\ (g\ x) $
We have:
Unfortunately, this problem is undecidable in general. There is a decidable fragment, known as Miller's Pattern Fragment. It's used extensively in, among other things, typechecking of dependently-typed programs with metavariables or pattern matching. This fragment is where unification variables are applied only to distinct bound program variables.
This paper provides a great tutorial of how higher order unification works, and walks through a (relatively) simple implementation of it.
Unfortunately, it doesn't look like your function falls into this pattern fragment. That said, what I'm looking seeing is pretty similar to function composition. Does the following function satisfy your property?
$B = \lambda f\ g\ x\ \ldotp f\ (g\ x) $
We have:
- $B\ f\ (\lambda x . M)$
- $= B\ f\ (\lambda y . [y/x]M)$ by $\alpha$-equivalence
- $ = \lambda x . f\ ((\lambda y. [y/x]M) x) $
- $= \lambda x . f\ ([x/y][y/x]M)$
- $= \lambda x . f\ M$
Context
StackExchange Computer Science Q#83662, answer score: 13
Revisions (0)
No revisions yet.