Can't use prefix symbols of arity > 1

[amelieled]

Take this Lambdapi formalization:

constant symbol wff : TYPE;

constant symbol taquet : wff → TYPE;
notation taquet prefix 40;

constant symbol implies : wff → wff → wff;
notation implies prefix 39;

constant symbol ax-1 : Π phi:wff, Π psi:wff, taquet implies phi implies psi phi;

Someone can obtain the following error:

[wff → wff] and [wff] are not unifiable.
Unification goals are unsatisfiable.

This appears probably because only unary symbol can be defined as prefix thanks to the command notation (even if it is not mention in the Lambdapi documentation).

Note: Documentation does not mention neither a definition for priority, nor an example to be sure about the definition considered in Lambdapi. Here, swaping 40 and 39 has no effect on the error, i.e. same error appears.

Note 2: Same error appears by writing constant symbol ax-1 : Π phi:wff, Π psi:wff, taquet (implies phi (implies psi phi));.

[amelieled]

Do you need more information to solve the issue? This would improve the Metamath to Lambdapi translator (which, by the way, is not mentioned in your list of translators).

[fblanqui]

@01mf02 @gabrielhdt Do you have any idea about that?

Which list of translators are you talking about?

[01mf02]

This appears probably because only unary symbol can be defined as prefix thanks to the command notation (even if it is not mention in the Lambdapi documentation).

@amelieled, it would be useful to be sure about the source of the error first. I suppose that this problem appears when checking ax-1? Can you confirm that checking a parenthesised version of ax-1 succeeds? I guess it should be taquet (implies phi (implies psi phi))?

I suppose that the parser does not consider the type of a symbol when determining precedences etc. That's why it probably parses something like implies (phi (implies psi phi)) or something like that.

[amelieled]

Which list of translators are you talking about?

https://github.com/Deducteam/lambdapi/blob/master/README.md or https://deducteam.gitlabpages.inria.fr/software.html

it would be useful to be sure about the source of the error first. I suppose that this problem appears when checking ax-1?

Yes

Can you confirm that checking a parenthesised version of ax-1 succeeds? I guess it should be taquet (implies phi (implies psi phi))?

Same error with: constant symbol ax-1 : Π phi:wff, Π psi:wff, taquet (implies phi (implies psi phi));.

I suppose that the parser does not consider the type of a symbol when determining precedences etc. That's why it probably parses something like implies (phi (implies psi phi)) or something like that.

Yes, or considers that the symbol is unary.

[fblanqui]

Which list of translators are you talking about?

https://github.com/Deducteam/lambdapi/blob/master/README.md

You can make a PR.

[GuillaumeGen]

From https://github.com/Deducteam/lambdapi/blob/dfbb1a435c835975d90a1426f51ec9c351b3d043/doc/commands.rst?plain=1#L213:

• Non-operator application (such as f x where f and x are not operators) has a higher priority than any operator application. Hence, if - is declared as prefix, then - f x is always parsed - (f x), no matter the priority of - is.

Hence I feel that declaring priority of prefix (or postfix) multi-args symbol is not a good idea.

[amelieled]

This is embarrassing, because every defined symbol is prefix (and often with more than one argument), and you can not choose a priority level for them.

[amelieled]

To be more concrete:

constant symbol Pattern : TYPE;
constant symbol Positive : Pattern → Pattern → TYPE;
notation Positive prefix 40;

constant symbol toto xX yY : Positive xX yY;

Error from the last line, i.e. declaration of toto:

[Pattern → TYPE] and [TYPE] are not unifiable.
Unification goals are unsatisfiable.

because Positive is seen as a unary symbol due to command notation, whereas it is a binary symbol according to its type.

[amelieled]

I would like also to add that I'm waiting for almost 2 months that this issue be solved. I can understand that it can take time but I have no visibility if this issue will be solved soon or will be done in several years (like for other issues which have been opened by myself).

Could you clarify the status of this issue?

[fblanqui]

Hi Amélie. This issue won't be solved any time soon, if any, as there is a simple work around: simply don't use prefix notations for non-unary symbols. Best regards, Frédéric.

[amelieled]

Thanks for the answer. But I think the best solution is to raise an error when the command notation is used to a non-unary prefix/postfix symbol or to a non-binary suffix symbol, and add explicitly these restrictions in the documentation. Indeed, if this changement is not done, LP will continue to accept this file:

constant symbol Pattern : TYPE;
constant symbol Positive : Pattern → Pattern → TYPE;
notation Positive prefix 40;

Moreover, I would like also to underline that your solution is not a solution: it is a restriction of LP that has huge consequences for the translation of Metamath into Dedukti. More generally, this restriction considerably reduces the possibility of obtaining a human-readable LP file from another tool.

[fblanqui]

the Metamath to Lambdapi translator (which, by the way, is not mentioned in your list of translators).

Which list of translators are you talking about?

https://github.com/Deducteam/lambdapi/blob/master/README.md or https://deducteam.gitlabpages.inria.fr/software.html

You need to provide links. We cannot guess them.

[amelieled]

As I said in the message you just deleted, all the needed information are in the annual Inria reports.