This is a research implementation of optimal beta reduction (Asperti98), combining implementation ideas of BOHM (Asperti96) with engineering tricks of HVM (Taelin22).
The target language is pure untyped nondeterministic λ-calculus (Barendregt84), that is the language with function abstraction, function application, bound variables, and nondeterministic parallel binary choice. This machine aims to implement types as closures (Scott76) (increasing idempotent functions) together with a rich type system of closures (Obermeyer09). It remains to be seen whether this is feasible.
The engineering plan is to create a readable and easily debuggable Python runtime together with an equivalent but highly-optimized C runtime, similar to HVM's hybrid Rust+C architecture (Taelin22). This architecture allows unit tests to be written in Python.
- Asperti96
- Andrea Asperti, Cecilia Giovanetti, Andrea Naletto (1996) "The Bologna Optimal Higher-order Machine" (doi | code)
- Asperti98
- Andrea Asperti, Stefano Guerrini (1998) "The optimal implementation of functional programming languages" (doi)
- Barendregt84
- Hendrik Barendregt (1984) "The lambda calculus: its syntax and semantics"
- Obermeyer09
- Fritz Obermeyer (2009) "Automated equational reasoning in nondeterministic λ-calculi modulo theories H*" (pdf | old code | new code)
- Salikhmetov17
- Anton Salikhmetov (2017) "inet-lib: JavaScript Engine for Interaction Nets" (code | paper)
- Scott76
- Dana Scott (1976) "Datatypes as Lattices" (doi | pdf)
- Taelin22
- Victor Taelin et al. (2022) "Higher-order Virtual Machine (HVM)" (code | docs)
Copyright (c) 2022 Fritz Obermeyer.
NOHM is licensed under the Apache 2.0 License.