Well, suppose that I have a set of functional definitions (with a syntax tree) in church encoding :
true : λx -> λy -> x
false : λx -> λy -> y
Giving the definition λx -> λy -> y, it is very clear how to return the named definition, applying a matching with alpha-equivalence will be enough.
α true λx -> λy -> y = false
α false λx -> λy -> y = true
But consider the example below:
0 : λf λz -> x
succ : λn λf λx -> f (n f x)
3 : succ (succ (succ 0)))
So, when 3 suffers from beta-reduction it will unfold to some definition like :
3_unfolded : (λf -> (λx -> (f (f (f x))))) : (A -> A) -> A -> A
You can see the term can get bigger easily, of course, it is not a good way to represent pure data, because of the size of the term. So, I want to know if there is an algorithm able efficiently to rename again every definition after suffering evaluation. Them 3_unfolded will become (succ (succ (succ 0))) again by giving the set of definitions of natural church encoding (0, and succ only).
I know there are some side effects, like ambiguous representations, but let's ignore that (if you expand the same definition of succ and rename to succ_2, for example).
This is essentially the problem of beta-equivalence, and it’s undecidable in general; it also won’t necessarily produce usable output even when it could produce something, e.g. with some restrictions including strong normalisation. Therefore I think your best strategies here will be heuristic, because by default, reductions destroy information. The solutions are to retain information that you care about, or avoid needing information that’s gone. For instance:
Decouple the memory representation of terms from their LC representations, in particular cases where you care about efficiency and usability. For example, you can store and print a Church numeral as a Natural, while still allowing it to be converted to a function as needed. I think this is the most practical technical angle.
Retain information about the provenance of each term, and use that as a hint to reconstruct named terms. For example, if you know that a term arose by a given shape of beta-reduction, you can beta-expand/alpha-match to potentially rediscover an application of a function like succ. This may help in simple cases but I expect it will fall down in nontrivial programs.
Instead of considering this an algorithmic problem, consider it a usability design problem, and focus on methods of identifying useful information and presenting it clearly. For example, search for the largest matching function body that is also the most specific, e.g. a term might match both λx. x (identity) and λf. λx. f x (function application), but the latter is more specific, and even more specifically it can be a numeral (λs. λz. s z = 1); if there are multiple possibilities, present the most likely few.
Whenever you encounter a problem that’s undecidable for arbitrary programs, it’s worth remembering that humans write extremely non-arbitrary programs. So heuristic solutions can work remarkably well in practice.