Skip to content

Commit

Permalink
Document eta reduction.
Browse files Browse the repository at this point in the history
  • Loading branch information
FranchuFranchu committed Mar 14, 2024
1 parent 2be113d commit 8b05c59
Showing 1 changed file with 53 additions and 1 deletion.
54 changes: 53 additions & 1 deletion src/transform/eta_reduce.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,61 @@
//! Carries out simple eta-reduction, to reduce the amount of rewrites at runtime.
//!
//! ### Eta-equivalence
//!
//! In interaction combinators, there are some nets that are equivalent and
//! have no observable difference
//!
//! ![Image of eta-equivalence](https://i.postimg.cc/XYVxdMFW/image.png)
//!
//! This module implements the eta-equivalence rule at the top-left of the image above
//!
//! ```txt
//! /|-, ,-|\ eta_reduce
//! ---| | X | |-- ~~~~~~~~~~~~> -------------
//! \|-' '-|/
//! ```
//!
//! In hvm-core's AST representation, this reduction looks like this
//!
//! ```txt
//! {lab x y} ... {lab x y} ~~~~~~~~> x ..... x
//! ```
//!
//! Essentially, both occurrences of the same constructor are replaced by a
//! variable.
//!
//! ### The algorithm
//!
//! The code uses a two-pass O(n) algorithm, where `n` is the amount of nodes
//! in the AST
//!
//! In the first pass, a node-list is built out of an ordered traversal of the AST.
//! Crucially, the node list stores variable offsets instead of the variable's names
//! Since the AST's order is consistent, the ordering of nodes in the node list can be
//! reproduced with a traversal.
//!
//! This means that each occurrence of a vaiable is encoded with the offset in the node-list to

Check warning on line 37 in src/transform/eta_reduce.rs

View workflow job for this annotation

GitHub Actions / cspell

Unknown word (vaiable)
//! the _other_ occurrence of the variable.
//!
//! For example, if we start with the net: `[(x y) (x y)]`
//!
//! The resulting node list will look like this:
//!
//! `[Ctr(1), Ctr(0), Var(3), Var(3), Ctr(0), Var(-3), Var(-3)]`
//!
//! The second pass uses the node list to find repeated constructors. If a constructor's
//! children are both variables with the same offset, then we lookup that offset relative to
//! the constructor. If it is equal to the first constructor, it means both of them are equal
//! and they can be replaced with a variable.


use std::{collections::HashMap, ops::RangeFrom};

use crate::ast::{Net, Tree};

/// Converts `(x y), (x y)` into `x, x`.
impl Net {
/// Carries out simple eta-reduction
pub fn eta_reduce(&mut self) {
let mut phase1 = Phase1::default();
for tree in self.trees() {
Expand Down

0 comments on commit 8b05c59

Please sign in to comment.