search

rlepigre / pml

New version of the PML language and (classical) proof assistant
http://pml-lang.org
MIT License
20 stars 2 forks source link

PML can not always use function equalities that it learned #22

Open craff opened 6 years ago

craff commented 6 years ago

When we learn that functions are equal, we should keep that information: VN_LAbs should contain a list of functions.

This would allow to always deduce f x = g x from f = g

rlepigre commented 6 years ago

I don't understand why this would be required. If f = g, then it is immediate that f x = g x.

craff commented 6 years ago

Assume PML learns f = g prior to the creation of the term "f x", without loss of generality, let us assume that f points to g in the union find map. Then, forming the term "f x" (or "g x"), we will only compute "g x".

In PML one, abstraction nodes were carying a list of functions, just to compute both f x and g x and call "union" on the result.

craff commented 6 years ago

Mais, bon, on n'a pas d'exemple encore avec des hypothèses de la forme f = g, où f et g ne sont pas des variables ... Donc ça peut attendre.

rlepigre commented 6 years ago

OK, cool, j'avais pas pensé à ça !