Enzo Crance (May 19 2022 at 15:33): Enzo Crance (May 19 2022 at 15:33):Hello. I need to be able to identify a lambda-abstracted function application with another one, and I need to know which variables were given to the abstracted one afterwards. For example, identifying fun T => @eq T and @eq nat is possible by giving nat to the first one, identifying fun n => option (vec A n) and option (vec A 0) is possible by giving 0, etc.
Here is my method: I beta-reduce the abstracted term by adding fresh variables, keeping the list of variables somewhere, then I unify the reduced term with the second function application, term by term. The variables from the initial list are now all instantiated with values that make the unification possible.
It works with a toy example in an Elpi query, but unfortunately not in a more realistic context. Indeed, putting an equality between app [global const «bitvector», c0] and app [global const «bitvector», X0^2] fails. X0^2 is a fresh variable and c0 is a local variable (under a binder). Could the binder be responsible for the failure? If this is the case, do you have an idea how to proceed?
Thanks in advance.
% filling the term with fresh variables (X here)
pred fill-vars i:term, o:term, o:list term.
fill-vars (fun _ _ F) Out [X|Used] :- !,
fill-vars (F X) Out Used.
fill-vars T T [].
% just inspecting the 2 lists of arguments of the function application,
% I don't care about the length difference, just need to unify args one by one
% until one of the lists is empty
pred unify-args i:list term, i:list term.
unify-args [] _ :- !.
unify-args _ [] :- !.
unify-args [A|As] [A|Bs] :- !,
unify-args As Bs.
unify-args has both arguments in input mode but you are using a non linear pattern. Use output mode, or two distinct vars and unify them in the premises.
Input mode and non linear patterns (repeated variables) is non-defined behavior.
Your way of tackling the problem is sound, it should work.
Last updated: Oct 13 2024 at 01:02 UTC