Frédéric Blanqui
Frédéric Blanqui
It could be useful to include https://github.com/Deducteam/lambdapi/blob/master/docs/syntax_dedukti.bnf in Dedukti (this grammar is generated in https://github.com/Deducteam/lambdapi/blob/master/docs/Makefile).
But is this file automatically generated from the grammar?
Hello Gaspard. You are raising interesting questions about the control of the reduction engine. But could you please first motivate this extension: in which application do you need this? Second,...
"might need" doesn't look enough to me... And this could be fixed by (if needed) modifying the strategy of construction of decision trees, by privileging the linear rules to the...
I think that it will be easier to experiment with Gabriel's fork since there is only one function to modify (and no grammar change).
And perhaps the heuristic function currently implemented by Gabriel already manages this. @gabrielhdt , could you please comment on this?
Why the second rule is non-linear? What are the types of c and u? It may be an interesting example for @wujuihsuan2016 . If the second rule is required for...
This rewrite system is not confluent and thus should not be accepted.
LP is intended to be a proof assistant, not a rewrite engine. So, in this context, these rewrite rules are not acceptable. 1. I don't see the point. The aim...
François, Dedukti itself has never been thought as a rewriting engine alone. What you are talking about is not Dedukti, but dkmeta, the rewriting part of Dedukti. So, yes, these...