From 16fa54cc51da8d7ba77ff6cdbd84e484d6206139 Mon Sep 17 00:00:00 2001 From: mehbark Date: Sun, 17 Nov 2024 16:23:22 -0500 Subject: [PATCH] `LC` docs --- Cargo.lock | 58 +++++++++++++++++++++++++++++ Cargo.toml | 1 + src/lib.rs | 103 ++++++++++++++++++++++++++++++++++++++-------------- src/test.rs | 33 +++++++++++++++++ 4 files changed, 168 insertions(+), 27 deletions(-) create mode 100644 src/test.rs diff --git a/Cargo.lock b/Cargo.lock index 0a92ed5..aa7a65f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -5,3 +5,61 @@ version = 3 [[package]] name = "lc-to-iota" version = "0.1.0" +dependencies = [ + "thiserror", +] + +[[package]] +name = "proc-macro2" +version = "1.0.89" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "syn" +version = "2.0.87" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "thiserror" +version = "2.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c006c85c7651b3cf2ada4584faa36773bd07bac24acfb39f3c431b36d7e667aa" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "2.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f077553d607adc1caf65430528a576c757a71ed73944b66ebb58ef2bbd243568" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "unicode-ident" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" diff --git a/Cargo.toml b/Cargo.toml index 4a6eaa7..cbf103c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,3 +4,4 @@ version = "0.1.0" edition = "2021" [dependencies] +thiserror = "2.0.3" diff --git a/src/lib.rs b/src/lib.rs index 4e11624..0d010f1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -3,8 +3,12 @@ //! to a tree of [Iota (ι) combinators](https://en.wikipedia.org/wiki/Iota_and_Jot), //! represented by the [`Iota`] type. +#[cfg(test)] +mod test; + use core::fmt; -use std::{collections::HashSet, rc::Rc}; +use std::rc::Rc; +use thiserror::Error; #[derive(Debug, PartialEq, Eq)] pub enum Iota { @@ -12,42 +16,96 @@ pub enum Iota { Iota, } +#[derive(Debug, Error, PartialEq, Eq)] +pub enum IotaCompileError { + #[error("LC term has a free variable")] + FreeVar, +} + +impl TryFrom for Iota { + type Error = IotaCompileError; + + fn try_from(value: LC) -> Result { + todo!() + } +} + +/// A representation of the [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus), with +/// [de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index). #[derive(Debug, PartialEq, Eq)] pub enum LC { + /// A lambda abstraction; binds a new variable. Abs(Rc), + /// An application of a function to an argument. App(Rc, Rc), + /// A variable represented by a + /// [de Bruijn index](https://en.wikipedia.org/wiki/De_Bruijn_index). + /// + /// Zero refers to the closest abstraction, and each successive number refers to a + /// nested abstraction, as shown in this diagram: + /// ```text + /// ┌─────┐ + /// │ ┌─┐ │ + /// λ λ λ 0 1 2 + /// └─────────┘ + /// ``` Var(usize), } impl LC { + /// Applies this term to the given term. + /// + /// Often more ergonomic than [`LC::App`]. + /// # examples + /// ``` + /// # use lc_to_iota::LC::{Abs, App, Var}; + /// assert_eq!(Var(0).app(1), App(Var(0).into(), Var(1).into())); + /// ``` + #[must_use] pub fn app(self, x: impl Into) -> Self { Self::App(self.into(), x.into().into()) } + /// Adds an abstration around this term. + /// + /// Often more ergonomic than [`LC::Abs`], but is somewhat backwards. + /// # examples + /// ``` + /// # use lc_to_iota::LC::{Abs, App, Var}; + /// assert_eq!(Var(0).abs(), Abs(Var(0).into())); + /// ``` + #[must_use] pub fn abs(self) -> Self { Self::Abs(self.into()) } - pub fn has_free_vars(&self) -> bool { - // TODO: faster - !self.free_vars().is_empty() + /// Returns whether any variables are + /// [free](https://en.wikipedia.org/wiki/Free_variables_and_bound_variables) in self; + /// that is, whether any variables occur that are not bound by an abstraction. + /// + /// # Examples + /// ``` + /// # use lc_to_iota::LC::{Abs, App, Var}; + /// // x + /// let x = Var(0); + /// assert!(x.has_free()); + /// // λx.x + /// assert!(!x.abs().has_free()); + /// // λfx.f x + /// let apply = Var(1).app(0).abs().abs(); + /// assert!(!apply.has_free()); + /// ``` + #[must_use] + pub fn has_free(&self) -> bool { + self.has_free_past(0) } - // contextless free vars aren't that useful? - pub fn free_vars(&self) -> HashSet { - self.free_vars_past(0) - } - - fn free_vars_past(&self, bound: usize) -> HashSet { - // TODO: faster + fn has_free_past(&self, bound: usize) -> bool { match self { - LC::Abs(x) => x.free_vars_past(bound + 1), - LC::App(f, x) => { - let f_vars = f.free_vars_past(bound); - let x_vars = x.free_vars_past(bound); - &f_vars | &x_vars - } - LC::Var(_) => todo!(), + LC::Abs(x) => x.has_free_past(bound + 1), + LC::App(f, x) => f.has_free_past(bound) || x.has_free_past(bound), + // if nothing is bound (bound = 0), x is always free + LC::Var(x) => *x >= bound, } } } @@ -67,12 +125,3 @@ impl fmt::Display for LC { } } } - -#[test] -fn lc_display() { - let identity = LC::Var(0).abs(); - assert_eq!(identity.to_string(), "(λ 0)"); - - let apply = LC::Var(1).app(0).abs().abs(); - assert_eq!(apply.to_string(), "(λ (λ (1 0)))"); -} diff --git a/src/test.rs b/src/test.rs new file mode 100644 index 0000000..24bc621 --- /dev/null +++ b/src/test.rs @@ -0,0 +1,33 @@ +use crate::*; + +#[test] +fn lc_display() { + use LC::*; + let identity = Var(0).abs(); + assert_eq!(identity.to_string(), "(λ 0)"); + + let apply = Var(1).app(0).abs().abs(); + assert_eq!(apply.to_string(), "(λ (λ (1 0)))"); + assert_eq!(apply.to_string(), "(λ (λ (1 0)))"); +} + +#[test] +fn lc_free() { + use LC::*; + assert!(Var(0).has_free()); + assert!(!Var(0).abs().has_free()); + assert!(Var(1).app(0).abs().has_free()); + assert!(!Var(1).app(0).abs().abs().has_free()); + assert!(Var(0).app(1).abs().has_free()); + + for i in 0..10 { + assert!(Var(i).has_free()); + let mut term = Var(i); + + for _ in 0..=i { + term = term.abs(); + } + // var `n` with `n+1` abstractions is bound. + assert!(!term.has_free()); + } +}