4 ms·
The article mentions the inability to decide equality of functions. A paper [1] about proving properties of functional programs shows how to do that modulo halt
by thesz 5y ago
The article mentions the inability to decide equality of functions. A paper [1] about proving properties of functional programs shows how to do that modulo halting theorem. E.g., if (\x -> f x == g x) halts we can decide whether f and g are equal.
[1] http://xenon.kiam.ru/~roman/doc/2009-Klyuchnikov_Romanenko--Proving_the_Equivalence_of_Higher-Order_Terms_by_Means_of_Supercompilation--slides.pdf http://xenon.kiam.ru/~roman/doc/2009-Klyuchnikov_Romanenko--...
Basically, if supercompilation of the expression above results in a huge nested case that has either True as a result (termination) or an application of function (not terminated due to infinite data structures, for example), then functions are equivalent. Otherwise, if there is at least one False, they are not, the path to False provides a counterexample.
- bmc7505 5y agoOne of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work: [1]: https://github.com/ilya-klyuchnikov/mrsc https://github.com/ilya-klyuchnikov/mrsc [2]: https://github.com/ilya-klyuchnikov/ttlite https://github.com/ilya-klyuchnikov/ttlite
- ajkjk 5y agoAre we already calling it 'Meta' unironically?
- steego 5y agoTo be fair, people who work on supercompilers have been in the meta space long before it was ironic.
- rowanG077 5y agoSupercompilation has also been known as metacompilation for decades.
- guerrilla 5y agoIn this case by Meta I think they mean Facebook. Name change today in case you missed thar.
- mro_name 5y agoWhom? Metaface?
- noduerme 5y agoNo one should ever call that thing Meta. We have to draw the line somewhere. Facebook needs to be gratuitously dead named.