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: Jun 06 2023 at 22:01 UTC