lambdapi
lambdapi copied to clipboard
Deducteam
Renaming bound variables equal to a symbol name
The example
symbol Set: TYPE
set declared "η"
injective symbol η: Set ⇒ TYPE
symbol arr: Set ⇒ Set ⇒ Set
rule η (arr &X &Y) → (η &X) ⇒ (η &Y)
set infix right 6 "~>" ≔ arr
constant symbol t: Set ⇒ TYPE
constant symbol quote {T: Set}: η T ⇒ t T
constant symbol T: Set
symbol f: η (T ~> T)
compute λ(T: Set), quote {T ~> T} (λx:η T, x) // Succeeds
compute λ(T: Set), quote {T ~> T} (λx:η T, f x)
// Fails with [T] and [T] are not convertible.
Fails with the error message
[T] and [T] are not convertible
Is it solved by #328?
My mistake, there is no problem, I have a constant named T as well as a variable, so the type of f is η T ⇒ η T (where T is the constant), but the type of x is η T, where T is the variable.
Should we provide something to distinguish, or should the user be careful?
Right. But we could perhaps do something about this by providing some warning or by making sure that names used for printing bound variables are distinct from locally declared function symbols. @rlepigre @craff couldn't https://github.com/rlepigre/ocaml-bindlib/ provide such a feature? I remember some previous version of Bindlib had a function to exclude some identifiers.
Yeah, that is possible but currently Lambdapi is not set up of that. There is the Bindlib.*_in family of functions that can be used for that. However, I feel like that this is rather a user problem here. I would be kind of weird to rename variables that appear in the file.
One solution would be to introduce a syntactic distinction between symbols and variables, but I'm not sure how I feel about that.
In the current syntax:
symbol Set: TYPE;
injective symbol η: Set → TYPE;
symbol arr: Set → Set → Set;
rule η (arr $X $Y) ↪ (η $X) → (η $Y);
constant symbol t: Set → TYPE;
constant symbol quote [T: Set]: η T → t T;
constant symbol T: Set;
symbol f: η (arr T T);
compute λ(T: Set), quote [arr T T] (λ x:η T, x);
compute λ(T: Set), quote [arr T T] (λ x:η T, f x);