A small demo project performing normal-order evaluation of untyped lambda calculus terms. It wraps the library https://github.com/stfnw/lambda-calculus-full-reducing-krivine-machine into a small cli app. The library implements a full-reducing variant (KN) of the Krivine abstract machine; specifically the formulation in Á. GARCÍA-PÉREZ and P. NOGUEIRA, "The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus", Journal of Functional Programming, vol. 29, p. e7, 2019. doi:10.1017/S0956796819000017; Fig. 3. "A version of KN that works with closures with closed terms". (This repo is unaffiliated; goal is me learning).
Example run:
$ cargo run -- '((λa. (a a)) (λa. a))'
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.04s
Running `target/debug/lambda-calculus-full-reducing-krivine-machine-cli '((λa. (a a)) (λa. a))'`
parsed term:
named: ((λa. (a a)) (λa. a))
blc: 01000110100010
reduced term:
named: (λa. a)
blc: 0010