search

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

normalization by evaluation #8

Closed fredokun closed 3 years ago

fredokun commented 4 years ago

LaTTe uses an ad-hoc normalization algorithm. It is effective but it is slow and rather inelegant. A significant improvement on both aspects should be obtained by the use of a normalization by evaluation (nbe) approach. The idea is to let Clojure perform the normalization, based on the fact that it is a lambda-calculus inside

fredokun commented 3 years ago

This is supported since https://github.com/latte-central/latte-kernel/commit/b14e1b129ad277ef2580e270050c72ffe1763b12