anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Natural Numbers (un)curry Blow-Up #158

Open agureev opened 12 months ago

agureev commented 12 months ago

The current pipeline has good optimization going for it, especially with the STLC reducer. However, abstractly, the user may compiler some code with lambda subterms which are neither on the top nor being applied to. This will cause a huge blow-up that may not even withstand operations with 5-bit natural numbers, much less 24 or 32-bit ones.

We need to resolve this by either thinking about implementing primitive function types or changing the computation strategies for hom-object structures in Geb.