search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

Add pattern matching modulo eta ? #231

Open fblanqui opened 4 years ago

fblanqui commented 4 years ago

Currently, the following file is not accepted:

symbol R:TYPE
symbol sin:R⇒R
symbol D:(R⇒R)⇒(R⇒R)
rule D(λx,sin &F[x]) → λx:R,x
assert D sin ≡ λx:R,x
francoisthire commented 4 years ago

Can you detail a little about your needs for having matching modulo eta?

The problem I see with having matching modulo eta (or conversion modulo eta) is about the conservativity of the encodings. If the original system does not have eta, I suspect that the theorem will break at some point. So if such feature is added, maybe it should be better to have a switch to turn it off.

Then, do we know if eta might interfere with other features such as non-linearity?