This module implements virtual machines for nondeterministic extensional combinatory algebra and λ-calculus.
tl;dr
- nondeterminism + order oracle = types
- order oracle + reflection = a very strong foundation
The engineering strategy has been to get "types for free" by adding angelic nondeterminism to the language and implementing a theorem prover to weakly decide Scott ordering and to "garbage collect" concurrent continuations that are provably redundant. This theorem prover is limited, but approaches the Pi02 complete theory H*. Since we've put so much effort into this theorem prover, we put more effort into exposing the theorem prover through reflection. Reflection has to be very careful and work always through a quoting comonad that flattens out order. Once we have the order oracle and reflection, this system is very strong, capable of expressing the full arithmetic hierarchy.
- [Scott76] Dana Scott (1976) Datatypes as Lattices
- [Obermeyer09] Fritz Obermeyer (2009) Automated Equational Reasoning in Nondeterministic λ-Calculi Modulo Theories H*
- [Huet98] Gerard Huet (1998) Regular Bohm Trees
- [Feferman05] Solomon Feferman (2005) Predicativity
- [Fischer11] Sebastian Fischer, Oleg Kiselyov, Chung-Chieh Shan (2011) Purely functional lazy nondeterministic programming