search

argumentcomputer / radiya.rs

A Rust implementation of the Lean kernel
MIT License
11 stars 0 forks source link

Fastest Reduction of Functional Programs #2

Open johnchandlerburnham opened 2 years ago

johnchandlerburnham commented 2 years ago

We have a number of different options for how we want to reduce functional programs:

@gabriel-barrett's candidate is https://github.com/gabriel-barrett/rust-evaluator/blob/functional_implementation/src/lazy.rs

In Yatima we used the lambda-dag, bottom-up beta reduction model (https://www.ccs.neu.edu/home/wand/papers/shivers-wand-10.pdf), and had an experimental reducer based on the G-machine: https://github.com/yatima-inc/yatima/commit/9d0f66edd5ae557a44fe910992cf57e1d0a8c942

So, a good thing to do would be to figure out a way to benchmark these different models for Lean-shaped programs

johnchandlerburnham commented 2 years ago

Probably also worth investigating https://github.com/Kindelia/HVM