simple_semantics/
lambda.rs

1//! The module that defines the basic lambda calculus used to compose expressions in the langauge
2//! of thought.
3
4use crate::utils::ArgumentIterator;
5use std::{
6    collections::{HashSet, VecDeque},
7    fmt::{Debug, Display},
8    hash::Hash,
9    iter::empty,
10    marker::PhantomData,
11};
12use thiserror::Error;
13
14pub mod types;
15use types::{LambdaType, TypeError};
16
17pub(crate) type Bvar = usize;
18
19///Errors resulting from interacting with a lambda calculus expression.
20#[derive(Debug, Clone, Error, PartialEq, Eq)]
21pub enum LambdaError {
22    ///A function application which violates the type system
23    #[error("The free variable has type {free_var} while the argument is {arg}")]
24    BadFreeVariableApp {
25        ///The type of the free variable involved
26        free_var: LambdaType,
27        ///The argument applied to a free variable.
28        arg: LambdaType,
29    },
30    ///A free variable that violates the type sytem
31    #[error("The free variable has type {free_var} while its lambda takes {lambda}")]
32    BadFreeVariable {
33        ///The type of the free variable involved
34        free_var: LambdaType,
35        ///The argument applied to a free variable.
36        lambda: LambdaType,
37    },
38
39    ///An internally caused error if `DeBruijn` indices are invalid.
40    #[error(
41        "A bound variable {var:?} cannot have a DeBruijn index higher than its lambda depth ({depth})"
42    )]
43    BadBoundVariable {
44        ///The `DeBruijn` index
45        var: LambdaExprRef,
46        ///The depth of the expression
47        depth: usize,
48    },
49
50    ///Any internal type error.
51    #[error("Expression has type error ({0})")]
52    TypeError(#[from] TypeError),
53
54    ///An error caused by a failed reduction
55    #[error("Failed reduction: {0}")]
56    ReductionError(#[from] ReductionError),
57}
58
59///A conversion error used when converting to a [`RootedLambdaPool`] from a [`Vec<Option<LambdaExpr>>`]
60#[derive(Debug, Clone, Error, PartialEq, Eq)]
61pub enum LambdaTryFromError {
62    ///This error happens if the vector is not exclusively [`Some`].
63    #[error("The vec contains None")]
64    HasNone,
65}
66
67///An error from a faulty reduction
68#[derive(Debug, Clone, Error, PartialEq, Eq)]
69pub enum ReductionError {
70    ///A invalid reference to a [`LambdaExpr`] is passed.
71    #[error("{0:?} is not a valid ref!")]
72    NotValidRef(LambdaExprRef),
73    ///A reference to a [`LambdaExpr`] which is not an application is passed
74    #[error("{0:?} is not an application!")]
75    NotApplication(LambdaExprRef),
76
77    ///An application that doesn't apply a lambda expression
78    #[error("The left hand side of the application ({app:?}), {lhs:?} is not a lambda expression!")]
79    NotLambdaInApplication {
80        ///The entire application
81        app: LambdaExprRef,
82        ///The left hand side of the application, which should be but isn't a lambda expression
83        lhs: LambdaExprRef,
84    },
85
86    ///Any general malformed types.
87    #[error("Incorrect types: {0}")]
88    TypeError(#[from] TypeError),
89}
90
91///An index to a [`LambdaExpr`] in the lambda pool.
92#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash, PartialOrd, Ord)]
93pub struct LambdaExprRef(pub u32);
94
95///A trait which allows one to define a language of thought that interacts with the lambda
96///calculus. An example implementation can be found for [`crate::language::Expr`].
97pub trait LambdaLanguageOfThought {
98    ///The type of the executable syntax tree
99    type Pool;
100    ///Error for converting from [`RootedLambdaPool<T>`] to [`LambdaLanguageOfThought::Pool`]
101    type ConversionError;
102
103    ///Given an expression, get an iterator of its children
104    fn get_children(&self) -> impl Iterator<Item = LambdaExprRef>;
105
106    ///Update the references such that `LambdaExprRef(0)` is remapped to `LambdaExprRef(remap[0])`.
107    ///(Used in garbage collection).
108    fn remap_refs(&mut self, remap: &[usize]);
109
110    ///Returns true if this is somewhere that can bind variables (e.g. should we increment debruijn
111    ///indices
112    fn inc_depth(&self) -> bool;
113
114    ///Returns the type of the bound variable at an instruction
115    fn var_type(&self) -> Option<&LambdaType>;
116
117    ///Given a list of new references for all children of an expr, change its children.
118    fn change_children(&mut self, new_children: impl Iterator<Item = LambdaExprRef>);
119
120    ///Get the number of children of an expression.
121    fn n_children(&self) -> usize;
122
123    ///Get the return type of an expression.
124    fn get_type(&self) -> &LambdaType;
125
126    ///Get the type of all children in order.
127    fn get_arguments(&self) -> impl Iterator<Item = LambdaType>;
128
129    ///Checks whether an expression is commutative
130    fn commutative(&self) -> bool {
131        false
132    }
133
134    ///Checks if two expressions are the same, *ignoring* their subtrees (so different children
135    ///shouldn't matter)
136    fn same_expr(&self, other: &Self) -> bool;
137
138    ///Convert from a [`RootedLambdaPool<T>`] to [`LambdaLanguageOfThought::Pool`]. May return an
139    ///error if there are any lambda terms left in the [`RootedLambdaPool<T>`] (e.g. not fully
140    ///reduced).
141    fn to_pool(pool: RootedLambdaPool<Self>) -> Result<Self::Pool, Self::ConversionError>
142    where
143        Self: Sized;
144}
145
146impl LambdaLanguageOfThought for () {
147    type Pool = ();
148    type ConversionError = ();
149    fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
150        std::iter::empty()
151    }
152
153    fn n_children(&self) -> usize {
154        0
155    }
156
157    fn var_type(&self) -> Option<&LambdaType> {
158        None
159    }
160
161    fn same_expr(&self, _other: &Self) -> bool {
162        true
163    }
164
165    fn remap_refs(&mut self, _: &[usize]) {}
166
167    fn change_children(&mut self, _: impl Iterator<Item = LambdaExprRef>) {}
168
169    fn get_type(&self) -> &LambdaType {
170        unimplemented!()
171    }
172
173    fn inc_depth(&self) -> bool {
174        false
175    }
176
177    fn get_arguments(&self) -> impl Iterator<Item = LambdaType> {
178        empty()
179    }
180
181    fn to_pool(_: RootedLambdaPool<Self>) -> Result<Self::Pool, ()> {
182        Ok(())
183    }
184}
185
186///A free variable which can either be named or refered to by a integer.
187#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash, PartialOrd, Ord)]
188pub enum FreeVar<'a> {
189    ///A labeled free variable
190    Named(&'a str),
191    ///An anonymous free variable defined by an index.
192    Anonymous(usize),
193}
194
195impl Display for FreeVar<'_> {
196    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
197        match self {
198            FreeVar::Named(s) => write!(f, "{s}"),
199            FreeVar::Anonymous(t) => write!(f, "{t}"),
200        }
201    }
202}
203
204impl<'a> From<&'a str> for FreeVar<'a> {
205    fn from(value: &'a str) -> Self {
206        FreeVar::Named(value)
207    }
208}
209
210impl From<usize> for FreeVar<'_> {
211    fn from(value: usize) -> Self {
212        FreeVar::Anonymous(value)
213    }
214}
215
216#[derive(Debug, Clone, Eq, PartialEq, Hash, PartialOrd, Ord)]
217///The core expression type of a lambda term
218pub enum LambdaExpr<'a, T> {
219    ///A lambda of a given type.
220    Lambda(LambdaExprRef, LambdaType),
221    ///A variable bound by a lambda, labeled by its [De Bruijn index](https://en.wikipedia.org/wiki/De_Bruijn_index).
222    BoundVariable(Bvar, LambdaType),
223    ///A free variable (may be named or anonymous, see [`FreeVar`]).
224    FreeVariable(FreeVar<'a>, LambdaType),
225    ///The application of an argument to a function
226    Application {
227        ///The body of the function
228        subformula: LambdaExprRef,
229
230        ///The argument of the function
231        argument: LambdaExprRef,
232    },
233    ///Any expression which is not part of the lambda calculus directly (e.g. primitives). See
234    ///[`crate::Expr`] for an example.
235    LanguageOfThoughtExpr(T),
236}
237
238impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
239    pub(crate) fn var_type(&self) -> Option<&LambdaType> {
240        match self {
241            LambdaExpr::Lambda(_, lambda_type) => Some(lambda_type),
242            LambdaExpr::LanguageOfThoughtExpr(e) => e.var_type(),
243            LambdaExpr::BoundVariable(..)
244            | LambdaExpr::FreeVariable(..)
245            | LambdaExpr::Application { .. } => None,
246        }
247    }
248    pub(crate) fn inc_depth(&self) -> bool {
249        match self {
250            LambdaExpr::Lambda(..) => true,
251            LambdaExpr::LanguageOfThoughtExpr(e) => e.inc_depth(),
252            LambdaExpr::BoundVariable(..)
253            | LambdaExpr::FreeVariable(..)
254            | LambdaExpr::Application { .. } => false,
255        }
256    }
257
258    pub(crate) fn commutative(&self) -> bool {
259        match self {
260            LambdaExpr::LanguageOfThoughtExpr(e) => e.commutative(),
261            LambdaExpr::Lambda(..)
262            | LambdaExpr::BoundVariable(..)
263            | LambdaExpr::FreeVariable(..)
264            | LambdaExpr::Application { .. } => false,
265        }
266    }
267}
268
269#[derive(Debug, Clone)]
270///A lambda expression with its root defined.
271pub struct RootedLambdaPool<'src, T: LambdaLanguageOfThought> {
272    pub(crate) pool: LambdaPool<'src, T>,
273    pub(crate) root: LambdaExprRef,
274}
275
276impl<T: PartialEq + LambdaLanguageOfThought> PartialEq for RootedLambdaPool<'_, T> {
277    fn eq(&self, other: &Self) -> bool {
278        let mut bfs = self.pool.bfs_from(self.root).map(|(x, _)| self.pool.get(x));
279        let mut o_bfs = other
280            .pool
281            .bfs_from(other.root)
282            .map(|(x, _)| other.pool.get(x));
283        loop {
284            let x = bfs.next();
285            let y = o_bfs.next();
286            match (x, y) {
287                (None, None) => return true,
288                (None, Some(_)) | (Some(_), None) => return false,
289                (Some(a), Some(b)) => {
290                    if !a.same_expr(b) {
291                        return false;
292                    }
293                }
294            }
295        }
296    }
297}
298
299impl<T: LambdaLanguageOfThought + HashLambda> Hash for RootedLambdaPool<'_, T> {
300    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
301        for x in self.pool.bfs_from(self.root).map(|(x, _)| self.pool.get(x)) {
302            match x {
303                LambdaExpr::Lambda(_, lambda_type) => {
304                    0.hash(state);
305                    lambda_type.hash(state);
306                }
307                LambdaExpr::BoundVariable(a, lambda_type) => {
308                    1.hash(state);
309                    a.hash(state);
310                    lambda_type.hash(state);
311                }
312                LambdaExpr::FreeVariable(free_var, lambda_type) => {
313                    2.hash(state);
314                    free_var.hash(state);
315                    lambda_type.hash(state);
316                }
317                LambdaExpr::Application { .. } => {
318                    3.hash(state);
319                }
320                LambdaExpr::LanguageOfThoughtExpr(x) => {
321                    4.hash(state);
322                    x.hash_expr(state);
323                }
324            }
325        }
326    }
327}
328
329///In order to hash a [`RootedLambdaPool`], this trait must be implemented.
330///It allows trees to be hashed without regard for the precise layout of their pools, only the
331///actual tree.
332pub trait HashLambda {
333    ///Hash the expression (without paying attention to subtrees which should be handled
334    ///[`RootedLambdaPool`]'s hash implementation)
335    fn hash_expr<H: std::hash::Hasher>(&self, state: &mut H);
336}
337
338impl<T: PartialEq + Eq + LambdaLanguageOfThought> Eq for RootedLambdaPool<'_, T> {}
339
340impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
341    fn same_expr(&self, other: &Self) -> bool {
342        match self {
343            LambdaExpr::Lambda(_, lambda_type) => {
344                matches!(other, LambdaExpr::Lambda(_, other_type) if lambda_type == other_type)
345            }
346            LambdaExpr::BoundVariable(x, a) => {
347                matches!(other, LambdaExpr::BoundVariable(y, b) if x==y && a==b)
348            }
349            LambdaExpr::FreeVariable(free_var, lambda_type) => {
350                matches!(other, LambdaExpr::FreeVariable(o_var, o_type) if o_var == free_var && o_type == lambda_type)
351            }
352            LambdaExpr::Application { .. } => matches!(self, LambdaExpr::Application { .. }),
353            LambdaExpr::LanguageOfThoughtExpr(x) => {
354                matches!(other, LambdaExpr::LanguageOfThoughtExpr(y) if x.same_expr(y))
355            }
356        }
357    }
358}
359
360impl<'src, T: LambdaLanguageOfThought> RootedLambdaPool<'src, T> {
361    ///Creates an anonymous free variable with [`index`] of type [`t`]
362    #[must_use]
363    pub fn new_free_variable(index: usize, t: LambdaType) -> RootedLambdaPool<'src, T> {
364        RootedLambdaPool {
365            pool: LambdaPool(vec![LambdaExpr::FreeVariable(FreeVar::Anonymous(index), t)]),
366            root: LambdaExprRef(0),
367        }
368    }
369
370    ///Gets all free variables that must be bound in order to evaluate this lambda expression
371    pub fn free_variables(&self) -> impl Iterator<Item = (&FreeVar<'src>, &LambdaType)> {
372        self.pool.0.iter().filter_map(|x| {
373            if let LambdaExpr::FreeVariable(free_var, lambda_type) = x {
374                Some((free_var, lambda_type))
375            } else {
376                None
377            }
378        })
379    }
380
381    pub(crate) fn root(&self) -> LambdaExprRef {
382        self.root
383    }
384
385    ///Get the expression of a lambda term.
386    pub(crate) fn get(&self, x: LambdaExprRef) -> &LambdaExpr<'src, T> {
387        self.pool.get(x)
388    }
389
390    ///Get the length of a lambda tree
391    #[allow(clippy::len_without_is_empty)]
392    #[must_use]
393    pub fn len(&self) -> usize {
394        self.pool.0.len()
395    }
396}
397
398impl<'src, T: LambdaLanguageOfThought + Clone> RootedLambdaPool<'src, T> {
399    ///Clean up dangling references.
400    pub fn cleanup(&mut self) {
401        self.root = self.pool.cleanup(self.root);
402    }
403
404    ///The type of the lambda expression
405    pub fn get_type(&self) -> Result<LambdaType, TypeError> {
406        self.pool.get_type(self.root)
407    }
408
409    ///Create a new lambda expression.
410    pub(crate) fn new(pool: LambdaPool<'src, T>, root: LambdaExprRef) -> Self {
411        RootedLambdaPool { pool, root }
412    }
413
414    ///Split into the pool and root seperately.
415    pub(crate) fn split(self) -> (LambdaPool<'src, T>, LambdaExprRef) {
416        (self.pool, self.root)
417    }
418
419    ///Combine two lambda expressions by applying one to the other. Returns [`None`] if that is
420    ///impossible.
421    #[must_use]
422    pub fn merge(mut self, other: Self) -> Option<Self> {
423        let self_type = self.pool.get_type(self.root).expect("malformed type");
424        let other_type = other.pool.get_type(other.root).expect("malformed type");
425
426        let self_subformula = if self_type.can_apply(&other_type) {
427            true
428        } else if other_type.can_apply(&self_type) {
429            false
430        } else {
431            return None;
432        };
433
434        let (other_pool, other_root) = other.split();
435        let other_root = self.pool.extend_pool(other_root, other_pool);
436
437        self.root = self.pool.add(if self_subformula {
438            LambdaExpr::Application {
439                subformula: self.root,
440                argument: other_root,
441            }
442        } else {
443            LambdaExpr::Application {
444                subformula: other_root,
445                argument: self.root,
446            }
447        });
448
449        Some(self)
450    }
451
452    ///Reduce a lambda expression
453    pub fn reduce(&mut self) -> Result<(), ReductionError> {
454        self.pool.reduce(self.root)?;
455        Ok(())
456    }
457
458    ///Convert a lambda expression to its executable version (should only be done if there are only
459    ///[`LambdaExpr::LanguageOfThoughtExpr`] expressions.
460    pub fn into_pool(mut self) -> Result<T::Pool, T::ConversionError> {
461        self.cleanup();
462        T::to_pool(self)
463    }
464
465    ///Replace a free variable with a value.
466    pub fn bind_free_variable(
467        &mut self,
468        fvar: FreeVar<'src>,
469        replacement: RootedLambdaPool<'src, T>,
470    ) -> Result<(), LambdaError> {
471        let (other_pool, other_root) = replacement.split();
472        let other_root = self.pool.extend_pool(other_root, other_pool);
473        self.pool.bind_free_variable(self.root, fvar, other_root)?;
474        //self.root = self.pool.cleanup(self.root);
475        Ok(())
476    }
477
478    ///Replace a free variable by lambda abstracting it. (e.g. $P(x_{free})$ to $\lambda x P(x)$).
479    pub fn lambda_abstract_free_variable(
480        &mut self,
481        fvar: FreeVar<'src>,
482        lambda_type: LambdaType,
483        always_abstract: bool,
484    ) -> Result<(), LambdaError> {
485        self.reduce()?;
486        let vars = self
487            .pool
488            .bfs_from(self.root)
489            .filter_map(|(x, d)| match self.pool.get(x) {
490                LambdaExpr::FreeVariable(var, var_type) if *var == fvar => {
491                    if &lambda_type == var_type {
492                        Some(Ok((x, d)))
493                    } else {
494                        Some(Err(LambdaError::BadFreeVariable {
495                            free_var: var_type.clone(),
496                            lambda: lambda_type.clone(),
497                        }))
498                    }
499                }
500                _ => None,
501            })
502            .collect::<Result<Vec<_>, LambdaError>>()?;
503
504        if !vars.is_empty() || always_abstract {
505            for (x, lambda_depth) in vars {
506                *self.pool.get_mut(x) =
507                    LambdaExpr::BoundVariable(lambda_depth, lambda_type.clone());
508            }
509            self.root = self.pool.add(LambdaExpr::Lambda(self.root, lambda_type));
510        }
511        Ok(())
512    }
513
514    ///Apply a free variable to a function.
515    pub fn apply_new_free_variable(
516        &mut self,
517        fvar: FreeVar<'src>,
518    ) -> Result<LambdaType, LambdaError> {
519        let pool_type = self.pool.get_type(self.root)?;
520        let var_type = pool_type.lhs()?;
521        let argument = self
522            .pool
523            .add(LambdaExpr::FreeVariable(fvar, var_type.clone()));
524        self.root = self.pool.add(LambdaExpr::Application {
525            subformula: self.root,
526            argument,
527        });
528        self.reduce()?;
529        Ok(var_type.clone())
530    }
531}
532
533#[derive(Default, Debug, Clone, Eq, PartialEq, Hash)]
534pub(crate) struct LambdaPool<'a, T: LambdaLanguageOfThought>(pub(crate) Vec<LambdaExpr<'a, T>>);
535
536impl<'src, T: LambdaLanguageOfThought + Sized> LambdaPool<'src, T> {
537    pub(crate) fn extend_pool(
538        &mut self,
539        mut other_root: LambdaExprRef,
540        mut other_pool: LambdaPool<'src, T>,
541    ) -> LambdaExprRef {
542        let shift_n = self.0.len();
543        let remap: Vec<_> = (0..other_pool.0.len()).map(|x| x + shift_n).collect();
544        other_pool.0.iter_mut().for_each(|x| x.remap_refs(&remap));
545        other_root.0 += shift_n as u32;
546        self.0.append(&mut other_pool.0);
547        other_root
548    }
549
550    ///Convert from [`Vec<LambdaExpr<T>>`] to [`LambdaPool`]
551    pub fn from(x: Vec<LambdaExpr<'src, T>>) -> Self {
552        LambdaPool(x)
553    }
554
555    ///Create a new, empty [`LambdaPool`]
556    pub fn new<'c>() -> LambdaPool<'c, T> {
557        LambdaPool(vec![])
558    }
559
560    fn checked_get(&self, expr: LambdaExprRef) -> Option<&LambdaExpr<'src, T>> {
561        self.0.get(expr.0 as usize)
562    }
563
564    ///Get the [`LambdaExpr`] at an index.
565    pub fn get(&self, expr: LambdaExprRef) -> &LambdaExpr<'src, T> {
566        &self.0[expr.0 as usize]
567    }
568
569    pub fn get_mut<'a>(&'a mut self, expr: LambdaExprRef) -> &'a mut LambdaExpr<'src, T> {
570        &mut self.0[expr.0 as usize]
571    }
572
573    pub fn add(&mut self, expr: LambdaExpr<'src, T>) -> LambdaExprRef {
574        let idx = self.0.len();
575        self.0.push(expr);
576        LambdaExprRef(idx.try_into().expect("Too many exprs in the pool"))
577    }
578}
579
580///Iterate over a lambda pool in breadth-first search
581pub(crate) struct LambdaPoolBFSIterator<'a, 'src, T: LambdaLanguageOfThought> {
582    pool: &'a LambdaPool<'src, T>,
583    queue: VecDeque<(LambdaExprRef, Bvar)>,
584}
585
586impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
587    pub(crate) fn n_children(&self) -> usize {
588        match self {
589            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => 0,
590            LambdaExpr::Lambda(..) => 1,
591            LambdaExpr::Application { .. } => 2,
592            LambdaExpr::LanguageOfThoughtExpr(e) => e.n_children(),
593        }
594    }
595
596    pub(crate) fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
597        match self {
598            LambdaExpr::Lambda(x, _) => ArgumentIterator::A([x].into_iter().copied()),
599            LambdaExpr::Application {
600                subformula,
601                argument,
602            } => ArgumentIterator::B([subformula, argument].into_iter().copied()),
603            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => {
604                ArgumentIterator::C(std::iter::empty())
605            }
606            LambdaExpr::LanguageOfThoughtExpr(x) => ArgumentIterator::D(x.get_children()),
607        }
608    }
609}
610
611impl<T: LambdaLanguageOfThought> Iterator for LambdaPoolBFSIterator<'_, '_, T> {
612    type Item = (LambdaExprRef, Bvar);
613
614    fn next(&mut self) -> Option<Self::Item> {
615        if let Some((x, lambda_depth)) = self.queue.pop_front() {
616            match self.pool.get(x) {
617                LambdaExpr::Lambda(x, _) => self.queue.push_back((*x, lambda_depth + 1)),
618                LambdaExpr::Application {
619                    subformula,
620                    argument,
621                } => {
622                    self.queue.push_back((*subformula, lambda_depth));
623                    self.queue.push_back((*argument, lambda_depth));
624                }
625                LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
626                LambdaExpr::LanguageOfThoughtExpr(x) => {
627                    let depth = lambda_depth + usize::from(x.inc_depth());
628
629                    x.get_children()
630                        .for_each(|x| self.queue.push_back((x, depth)));
631                }
632            }
633            Some((x, lambda_depth))
634        } else {
635            None
636        }
637    }
638}
639
640///Iterate over a lambda pool and return a mutable reference
641pub(crate) struct MutableLambdaPoolBFSIterator<'a, 'src: 'a, T: LambdaLanguageOfThought + 'a> {
642    pool: *mut LambdaPool<'src, T>,
643    queue: VecDeque<(LambdaExprRef, Bvar)>,
644    phantom: PhantomData<&'a ()>,
645}
646
647impl<'a, 'src: 'a, T: LambdaLanguageOfThought + 'a> MutableLambdaPoolBFSIterator<'a, 'src, T> {
648    fn new(pool: &mut LambdaPool<'src, T>, x: LambdaExprRef) -> Self {
649        Self {
650            pool: std::ptr::from_mut::<LambdaPool<'src, T>>(pool),
651            queue: VecDeque::from([(x, 0)]),
652            phantom: PhantomData,
653        }
654    }
655}
656
657impl<'a, 'src, T: LambdaLanguageOfThought> Iterator for MutableLambdaPoolBFSIterator<'a, 'src, T> {
658    type Item = (&'a mut LambdaExpr<'src, T>, usize, LambdaExprRef);
659
660    fn next(&mut self) -> Option<Self::Item> {
661        if let Some((x, lambda_depth)) = self.queue.pop_front() {
662            let expr = unsafe { self.pool.as_ref().unwrap() };
663            match expr.get(x) {
664                LambdaExpr::Lambda(x, _) => self.queue.push_back((*x, lambda_depth + 1)),
665                LambdaExpr::Application {
666                    subformula,
667                    argument,
668                } => {
669                    self.queue.push_back((*subformula, lambda_depth));
670                    self.queue.push_back((*argument, lambda_depth));
671                }
672                LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
673                LambdaExpr::LanguageOfThoughtExpr(x) => {
674                    let depth = lambda_depth + usize::from(x.inc_depth());
675
676                    x.get_children()
677                        .for_each(|x| self.queue.push_back((x, depth)));
678                }
679            }
680            Some((
681                unsafe { self.pool.as_mut().unwrap().get_mut(x) },
682                lambda_depth,
683                x,
684            ))
685        } else {
686            None
687        }
688    }
689}
690
691impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T> {
692    pub(crate) fn bfs_from(&self, x: LambdaExprRef) -> LambdaPoolBFSIterator<'_, 'src, T> {
693        LambdaPoolBFSIterator {
694            pool: self,
695            queue: VecDeque::from([(x, 0)]),
696        }
697    }
698}
699impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T> {
700    pub fn get_type(&self, x: LambdaExprRef) -> Result<LambdaType, TypeError> {
701        match self.get(x) {
702            LambdaExpr::BoundVariable(_, x) | LambdaExpr::FreeVariable(_, x) => Ok(x.clone()),
703            LambdaExpr::Lambda(s, x) => {
704                let result = self.get_type(*s);
705                Ok(LambdaType::compose(x.clone(), result?))
706            }
707            LambdaExpr::Application { subformula, .. } => {
708                let subformula_type = self.get_type(*subformula)?;
709                Ok(subformula_type.rhs()?.clone())
710            }
711            LambdaExpr::LanguageOfThoughtExpr(x) => Ok(x.get_type().clone()),
712        }
713    }
714
715    fn check_type_clash(&self, x: LambdaExprRef) -> Result<LambdaType, ReductionError> {
716        if let LambdaExpr::Application {
717            subformula,
718            argument,
719        } = self.get(x)
720        {
721            let argument_type = self.get_type(*argument)?;
722            let subformula_type = self.get_type(*subformula)?;
723            Ok(subformula_type.apply(&argument_type)?.clone())
724        } else {
725            Err(ReductionError::NotApplication(x))
726        }
727    }
728
729    pub(crate) fn bfs_from_mut<'a>(
730        &'a mut self,
731        x: LambdaExprRef,
732    ) -> MutableLambdaPoolBFSIterator<'a, 'src, T> {
733        MutableLambdaPoolBFSIterator::new(self, x)
734    }
735
736    fn get_next_app(&self, root: LambdaExprRef) -> Option<LambdaExprRef> {
737        self.bfs_from(root)
738            .map(|(x, _)| x)
739            .find(|x| match self.get(*x) {
740                LambdaExpr::Application { subformula, .. } => {
741                    matches!(self.get(*subformula), LambdaExpr::Lambda(..))
742                }
743                _ => false,
744            })
745    }
746}
747
748impl<'src, T: LambdaLanguageOfThought> LambdaPool<'src, T>
749where
750    T: Clone,
751{
752    fn bind_free_variable(
753        &mut self,
754        root: LambdaExprRef,
755        fvar: FreeVar<'src>,
756        replacement_root: LambdaExprRef,
757    ) -> Result<(), LambdaError> {
758        let arg_t = self.get_type(replacement_root)?;
759
760        let to_replace = self
761            .bfs_from(root)
762            .filter_map(|(x, d)| match self.get(x) {
763                LambdaExpr::FreeVariable(var, t) if *var == fvar => {
764                    if t == &arg_t {
765                        Some(Ok((x, d)))
766                    } else {
767                        Some(Err(LambdaError::BadFreeVariableApp {
768                            free_var: t.clone(),
769                            arg: arg_t.clone(),
770                        }))
771                    }
772                }
773                _ => None,
774            })
775            .collect::<Result<Vec<_>, LambdaError>>()?;
776
777        self.replace_section(&to_replace, replacement_root);
778        Ok(())
779    }
780
781    fn replace_section(&mut self, to_replace: &[(LambdaExprRef, usize)], to_copy: LambdaExprRef) {
782        let n = to_replace.len();
783        for (i, (x, depth)) in to_replace.iter().enumerate() {
784            if i == n - 1 {
785                for (x, d, _) in self.bfs_from_mut(to_copy) {
786                    if let LambdaExpr::BoundVariable(bound_depth, _) = x
787                        && *bound_depth >= d
788                    {
789                        *bound_depth += depth;
790                    }
791                }
792                //Last iteration so we don't need to copy anymore.
793                *self.get_mut(*x) = self.get(to_copy).clone();
794            } else {
795                let mut len = self.0.len();
796                let mut first = true;
797                let mut head = None;
798                self.0.extend(
799                    self.bfs_from(to_copy)
800                        .filter_map(|(x, d)| {
801                            let mut expr = self.get(x).clone();
802                            if let LambdaExpr::BoundVariable(bound_depth, _) = &mut expr
803                                && *bound_depth >= d
804                            {
805                                *bound_depth += depth;
806                            }
807
808                            let old_len = len;
809                            len += expr.n_children();
810                            expr.change_children((old_len..len).map(|x| LambdaExprRef(x as u32)));
811                            if first {
812                                head = Some(expr);
813                                first = false;
814                                None
815                            } else {
816                                Some(expr)
817                            }
818                        })
819                        .collect::<Vec<_>>(),
820                );
821
822                *self.get_mut(*x) = head.unwrap();
823            }
824        }
825    }
826
827    fn beta_reduce(&mut self, app: LambdaExprRef) -> Result<(), ReductionError> {
828        //BFS over all children and then replace debruijn k w/ argument ref where k is the number
829        //of lambda abstractions we've gone under, e.g. (lambda 0 lambda 0 1)(u) -> lambda u lambda
830        //1
831        //
832        //swap position of lambda ref and subformula ref so the lambda now leads to this.
833        //
834        let Some(expr) = self.checked_get(app) else {
835            return Err(ReductionError::NotValidRef(app));
836        };
837
838        let (inner_term, argument, subformula_vars) = if let LambdaExpr::Application {
839            argument,
840            subformula,
841        } = expr
842        {
843            let inner_term = match self.get(*subformula) {
844                LambdaExpr::Lambda(x, ..) => {
845                    self.check_type_clash(app)?;
846                    *x
847                }
848                _ => {
849                    return Err(ReductionError::NotLambdaInApplication {
850                        app,
851                        lhs: *subformula,
852                    });
853                }
854            };
855
856            (
857                inner_term,
858                *argument,
859                self.bfs_from_mut(inner_term)
860                    .filter_map(|(expr, d, expr_ref)| {
861                        if let LambdaExpr::BoundVariable(b_d, _) = expr {
862                            if *b_d > d {
863                                //Decrement locally free variables
864                                *b_d -= 1;
865                                None
866                            } else if *b_d == d {
867                                Some((expr_ref, *b_d))
868                            } else {
869                                None
870                            }
871                        } else {
872                            None
873                        }
874                    })
875                    .collect::<Vec<_>>(),
876            )
877        } else {
878            return Err(ReductionError::NotApplication(app));
879        };
880
881        //We used to swap this, but that will cause an insanely arcane bug.
882        //This is because the same term may be referred to by multiple instructions so if you swap
883        //them, it gets invalidated.
884        self.replace_section(&subformula_vars, argument);
885        self.0[app.0 as usize] = self.0[inner_term.0 as usize].clone();
886        //self.0.swap(inner_term.0 as usize, app.0 as usize); <- BAD
887
888        Ok(())
889    }
890
891    ///Iterates through a pool and de-allocates dangling refs and updates `ExprRefs` to new
892    ///addresses. Basically garbage collection.
893    pub(crate) fn cleanup(&mut self, root: LambdaExprRef) -> LambdaExprRef {
894        let findable: HashSet<_> = self.bfs_from(root).map(|(x, _)| x.0 as usize).collect();
895        let mut remap = (0..self.0.len()).collect::<Vec<_>>();
896        let mut adjustment = 0;
897
898        for i in &mut remap {
899            if findable.contains(i) {
900                *i -= adjustment;
901            } else {
902                adjustment += 1;
903            }
904        }
905
906        let mut i = 0;
907        self.0.retain(|_| {
908            i += 1;
909            findable.contains(&(i - 1))
910        });
911        for x in &mut self.0 {
912            x.remap_refs(&remap);
913        }
914        LambdaExprRef(remap[root.0 as usize] as u32)
915    }
916
917    pub fn reduce(&mut self, root: LambdaExprRef) -> Result<(), ReductionError> {
918        while let Some(x) = self.get_next_app(root) {
919            self.beta_reduce(x)?;
920        }
921        Ok(())
922    }
923}
924
925impl<T: LambdaLanguageOfThought> LambdaExpr<'_, T> {
926    pub(crate) fn change_children(&mut self, mut children: impl Iterator<Item = LambdaExprRef>) {
927        match self {
928            LambdaExpr::Lambda(lambda_expr_ref, _) => *lambda_expr_ref = children.next().unwrap(),
929            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
930            LambdaExpr::Application {
931                subformula,
932                argument,
933            } => {
934                *subformula = children.next().unwrap();
935                *argument = children.next().unwrap();
936            }
937            LambdaExpr::LanguageOfThoughtExpr(x) => x.change_children(children),
938        }
939    }
940
941    fn remap_refs(&mut self, remap: &[usize]) {
942        match self {
943            LambdaExpr::Lambda(x, _) => {
944                *x = LambdaExprRef(remap[x.0 as usize] as u32);
945            }
946            LambdaExpr::Application {
947                subformula,
948                argument,
949            } => {
950                *subformula = LambdaExprRef(remap[subformula.0 as usize] as u32);
951                *argument = LambdaExprRef(remap[argument.0 as usize] as u32);
952            }
953            LambdaExpr::BoundVariable(..) | LambdaExpr::FreeVariable(..) => (),
954            LambdaExpr::LanguageOfThoughtExpr(x) => x.remap_refs(remap),
955        }
956    }
957}
958
959///Details about a [`RootedLambdaPool`]
960#[derive(Debug, Clone, PartialEq, Eq, Hash)]
961pub enum LambdaSummaryStats {
962    ///The expression is correctly formed.
963    WellFormed {
964        ///What type is it
965        lambda_type: LambdaType,
966
967        ///Is it a constant function?
968        constant_function: bool,
969
970        ///How long is the expression?
971        n_nodes: usize,
972    },
973
974    ///Is there a problem with the expression
975    Malformed,
976}
977
978impl<T: LambdaLanguageOfThought + Clone + std::fmt::Debug> RootedLambdaPool<'_, T> {
979    ///Convert an expression `phi` of type `x` and convert it to `lambda <x,t> P P(phi)`
980    pub fn lift(&mut self) -> Result<(), TypeError> {
981        let t =
982            LambdaType::Composition(Box::new(self.get_type()?.clone()), Box::new(LambdaType::T));
983
984        let p = self.pool.add(LambdaExpr::BoundVariable(0, t.clone()));
985        let apply = self.pool.add(LambdaExpr::Application {
986            subformula: p,
987            argument: self.root,
988        });
989        let lambda = self.pool.add(LambdaExpr::Lambda(apply, t));
990        self.root = lambda;
991
992        Ok(())
993    }
994
995    ///Get [`LambdaSummaryStats`] for an expression, e.g. how many context functions, size, etc.
996    #[must_use]
997    pub fn stats(&self) -> LambdaSummaryStats {
998        let lambda_type = self.get_type();
999        if lambda_type.is_err() {
1000            return LambdaSummaryStats::Malformed;
1001        }
1002        let lambda_type = lambda_type.unwrap();
1003        let n_nodes = self.pool.0.len();
1004
1005        match self.all_lambda_has_variable(self.root) {
1006            Ok(has_variable) => LambdaSummaryStats::WellFormed {
1007                lambda_type,
1008                constant_function: !has_variable,
1009                n_nodes,
1010            },
1011
1012            Err(_) => LambdaSummaryStats::Malformed,
1013        }
1014    }
1015
1016    fn all_lambda_has_variable(&self, i: LambdaExprRef) -> Result<bool, LambdaError> {
1017        let mut found = vec![];
1018        let mut stack = vec![(i, vec![])];
1019        while let Some((expr_ref, mut lambdas)) = stack.pop() {
1020            match self.get(expr_ref) {
1021                LambdaExpr::Lambda(lambda_expr_ref, _) => {
1022                    found.push(false);
1023                    lambdas.push(found.len() - 1);
1024                    stack.push((*lambda_expr_ref, lambdas));
1025                }
1026                LambdaExpr::BoundVariable(d, _) => {
1027                    if let Some(index) = lambdas.len().checked_sub(d + 1) {
1028                        if let Some(found_index) = lambdas.get(index) {
1029                            if let Some(found) = found.get_mut(*found_index) {
1030                                *found = true;
1031                            } else {
1032                                return Err(LambdaError::BadBoundVariable {
1033                                    var: expr_ref,
1034                                    depth: lambdas.len(),
1035                                });
1036                            }
1037                        } else {
1038                            return Err(LambdaError::BadBoundVariable {
1039                                var: expr_ref,
1040                                depth: lambdas.len(),
1041                            });
1042                        }
1043                    } else {
1044                        return Err(LambdaError::BadBoundVariable {
1045                            var: expr_ref,
1046                            depth: lambdas.len(),
1047                        });
1048                    }
1049                }
1050                LambdaExpr::FreeVariable(..) => (),
1051                LambdaExpr::Application {
1052                    subformula,
1053                    argument,
1054                } => {
1055                    stack.push((*subformula, lambdas.clone()));
1056                    stack.push((*argument, lambdas));
1057                }
1058
1059                LambdaExpr::LanguageOfThoughtExpr(x) => {
1060                    if x.inc_depth() {
1061                        found.push(false);
1062                        lambdas.push(found.len() - 1);
1063                    }
1064                    stack.extend(x.get_children().map(|x| (x, lambdas.clone())));
1065                }
1066            }
1067        }
1068
1069        Ok(found.iter().all(|x| *x))
1070    }
1071}
1072
1073impl<'a, T: LambdaLanguageOfThought> From<LambdaPool<'a, T>> for Vec<Option<LambdaExpr<'a, T>>> {
1074    fn from(value: LambdaPool<'a, T>) -> Self {
1075        value.0.into_iter().map(Some).collect()
1076    }
1077}
1078
1079impl<'a, T: LambdaLanguageOfThought> TryFrom<Vec<Option<LambdaExpr<'a, T>>>> for LambdaPool<'a, T> {
1080    type Error = LambdaTryFromError;
1081
1082    fn try_from(value: Vec<Option<LambdaExpr<'a, T>>>) -> Result<Self, Self::Error> {
1083        match value.into_iter().collect::<Option<Vec<_>>>() {
1084            Some(x) => Ok(LambdaPool(x)),
1085            None => Err(LambdaTryFromError::HasNone),
1086        }
1087    }
1088}
1089
1090#[cfg(test)]
1091mod test {
1092
1093    use std::hash::{DefaultHasher, Hasher};
1094
1095    use super::*;
1096    use crate::language::{
1097        ActorOrEvent, BinOp, Expr, ExprPool, ExprRef, LanguageExpression, MonOp,
1098    };
1099
1100    #[test]
1101    fn stats() -> anyhow::Result<()> {
1102        for (expr, constant_lambda) in [
1103            ("a_0", false),
1104            ("lambda a x (pa_man(x))", false),
1105            ("lambda a x (pa_man(a_m))", true),
1106            (
1107                "lambda a x (((lambda a y (pa_woman(y)))(a_m)) & pa_man(x))",
1108                false,
1109            ),
1110            (
1111                "lambda a x (((lambda a y (pa_woman(a_m)))(a_m)) & pa_man(x))",
1112                true,
1113            ),
1114            ("lambda a y (pa_woman(a_m))", true),
1115            ("lambda a y (lambda a x (y))", true),
1116            ("some(x, pa_man(x), True)", false),
1117            ("some(x, pa_man(x), pa_man(x))", false),
1118            ("some(x, True, pa_man(x))", false),
1119            ("some(x, True, True)", true),
1120        ] {
1121            let expr = RootedLambdaPool::parse(expr)?;
1122            match expr.stats() {
1123                LambdaSummaryStats::WellFormed {
1124                    constant_function, ..
1125                } => assert_eq!(constant_function, constant_lambda),
1126                LambdaSummaryStats::Malformed => panic!("{expr} should be well-formed!"),
1127            }
1128        }
1129        Ok(())
1130    }
1131
1132    fn k<'a, T: Default>(pos: u32) -> anyhow::Result<[LambdaExpr<'a, T>; 3]> {
1133        Ok([
1134            LambdaExpr::Lambda(LambdaExprRef(pos + 1), LambdaType::e().clone()),
1135            LambdaExpr::Lambda(LambdaExprRef(pos + 2), LambdaType::e().clone()),
1136            LambdaExpr::BoundVariable(1, LambdaType::e().clone()),
1137        ])
1138    }
1139
1140    #[test]
1141    fn complicated_lambda_language_of_thought() -> anyhow::Result<()> {
1142        let mut pool = LambdaPool::<Expr>(vec![
1143            LambdaExpr::Application {
1144                //John dances
1145                subformula: LambdaExprRef(1),
1146                argument: LambdaExprRef(4),
1147            },
1148            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1149            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1150                MonOp::Property("32", ActorOrEvent::Actor),
1151                ExprRef(3),
1152            )),
1153            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1154            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1155        ]);
1156        pool.reduce(LambdaExprRef(0))?;
1157        pool.cleanup(LambdaExprRef(0));
1158
1159        assert_eq!(
1160            pool.clone(),
1161            LambdaPool(vec![
1162                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1163                    MonOp::Property("32", ActorOrEvent::Actor),
1164                    ExprRef(1)
1165                )),
1166                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3"))
1167            ]),
1168        );
1169
1170        let mut pool = LambdaPool(vec![
1171            LambdaExpr::Application {
1172                subformula: LambdaExprRef(1),
1173                argument: LambdaExprRef(5),
1174            },
1175            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::from_string("<a, t>")?),
1176            LambdaExpr::Application {
1177                subformula: LambdaExprRef(3),
1178                argument: LambdaExprRef(4),
1179            },
1180            LambdaExpr::BoundVariable(0, LambdaType::et().clone()),
1181            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1182            LambdaExpr::Lambda(LambdaExprRef(6), LambdaType::a().clone()),
1183            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1184                MonOp::Property("36", ActorOrEvent::Actor),
1185                ExprRef(7),
1186            )),
1187            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1188        ]);
1189        pool.reduce(LambdaExprRef(0))?;
1190        pool.cleanup(LambdaExprRef(0));
1191        assert_eq!(
1192            pool,
1193            LambdaPool(vec![
1194                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1195                    MonOp::Property("36", ActorOrEvent::Actor),
1196                    ExprRef(1)
1197                )),
1198                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1199            ])
1200        );
1201
1202        let mut pool = LambdaPool(vec![
1203            LambdaExpr::Application {
1204                subformula: LambdaExprRef(1),
1205                argument: LambdaExprRef(6),
1206            },
1207            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::t().clone()),
1208            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::t().clone()),
1209            LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(4), ExprRef(5))), //10
1210            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1211            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1212            LambdaExpr::Application {
1213                //6
1214                subformula: LambdaExprRef(7),
1215                argument: LambdaExprRef(10),
1216            },
1217            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::a().clone()),
1218            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1219                MonOp::Property("36", ActorOrEvent::Actor),
1220                ExprRef(9),
1221            )),
1222            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1223            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1224        ]);
1225        pool.reduce(LambdaExprRef(0))?;
1226        pool.cleanup(LambdaExprRef(0));
1227
1228        assert_eq!(
1229            pool,
1230            LambdaPool(vec![
1231                LambdaExpr::Lambda(LambdaExprRef(1), LambdaType::t().clone()),
1232                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3))),
1233                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1234                    MonOp::Property("36", ActorOrEvent::Actor),
1235                    ExprRef(4)
1236                )),
1237                LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1238                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1239            ])
1240        );
1241
1242        // [[[Mary sings] and]  [John dances]]
1243        let mut pool = LambdaPool::<Expr>(vec![
1244            LambdaExpr::Application {
1245                subformula: LambdaExprRef(6),
1246                argument: LambdaExprRef(1),
1247            },
1248            LambdaExpr::Application {
1249                //John dances
1250                subformula: LambdaExprRef(2),
1251                argument: LambdaExprRef(5),
1252            },
1253            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::a().clone()),
1254            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1255                MonOp::Property("32", ActorOrEvent::Actor),
1256                ExprRef(4),
1257            )),
1258            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1259            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1260            // 6
1261            //\lambda x. Mary sings and
1262            LambdaExpr::Application {
1263                subformula: LambdaExprRef(7),
1264                argument: LambdaExprRef(12),
1265            },
1266            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::t().clone()),
1267            LambdaExpr::Lambda(LambdaExprRef(9), LambdaType::t().clone()),
1268            LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(10), ExprRef(11))), //10
1269            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1270            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1271            LambdaExpr::Application {
1272                //13
1273                subformula: LambdaExprRef(13),
1274                argument: LambdaExprRef(16),
1275            },
1276            LambdaExpr::Lambda(LambdaExprRef(14), LambdaType::a().clone()),
1277            LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1278                MonOp::Property("36", ActorOrEvent::Actor),
1279                ExprRef(15),
1280            )),
1281            LambdaExpr::BoundVariable(0, LambdaType::a().clone()),
1282            LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2")),
1283        ]);
1284        pool.reduce(LambdaExprRef(0))?;
1285        let root = pool.cleanup(LambdaExprRef(0));
1286        assert_eq!(
1287            pool,
1288            LambdaPool(vec![
1289                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3))),
1290                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("3")),
1291                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1292                    MonOp::Property("36", ActorOrEvent::Actor),
1293                    ExprRef(4)
1294                )),
1295                LambdaExpr::LanguageOfThoughtExpr(Expr::Unary(
1296                    MonOp::Property("32", ActorOrEvent::Actor),
1297                    ExprRef(1)
1298                )),
1299                LambdaExpr::LanguageOfThoughtExpr(Expr::Actor("2"))
1300            ])
1301        );
1302
1303        assert_eq!(
1304            RootedLambdaPool::new(pool, root).into_pool()?,
1305            LanguageExpression::new(
1306                ExprPool::from(vec![
1307                    Expr::Binary(BinOp::And, ExprRef(2), ExprRef(3)),
1308                    Expr::Actor("3"),
1309                    Expr::Unary(MonOp::Property("36", ActorOrEvent::Actor), ExprRef(4)),
1310                    Expr::Unary(MonOp::Property("32", ActorOrEvent::Actor), ExprRef(1)),
1311                    Expr::Actor("2")
1312                ]),
1313                ExprRef(root.0)
1314            )
1315        );
1316        Ok(())
1317    }
1318    #[test]
1319    fn type_check() -> anyhow::Result<()> {
1320        // [[[Mary sings] and]  [John dances]]
1321        let mut pool = LambdaPool::<()>(vec![
1322            LambdaExpr::Application {
1323                subformula: LambdaExprRef(1),
1324                argument: LambdaExprRef(3),
1325            },
1326            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1327            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1328            LambdaExpr::FreeVariable("0".into(), LambdaType::t().clone()),
1329        ]);
1330        assert_eq!(
1331            pool.reduce(LambdaExprRef(0)).unwrap_err(),
1332            ReductionError::TypeError(TypeError::CantApply(
1333                LambdaType::t().clone(),
1334                LambdaType::at().clone()
1335            ))
1336        );
1337
1338        let mut pool = LambdaPool::<()>(vec![
1339            LambdaExpr::Application {
1340                subformula: LambdaExprRef(1),
1341                argument: LambdaExprRef(3),
1342            },
1343            LambdaExpr::Lambda(LambdaExprRef(2), LambdaType::a().clone()),
1344            LambdaExpr::BoundVariable(0, LambdaType::t().clone()),
1345            LambdaExpr::FreeVariable("0".into(), LambdaType::a().clone()),
1346        ]);
1347        assert!(pool.reduce(LambdaExprRef(0)).is_ok());
1348        Ok(())
1349    }
1350
1351    #[test]
1352    fn complicated_lambda() -> anyhow::Result<()> {
1353        // [[[Mary sings] and]  [John dances]]
1354        let mut pool = LambdaPool::<()>(vec![
1355            LambdaExpr::Application {
1356                subformula: LambdaExprRef(5),
1357                argument: LambdaExprRef(1),
1358            },
1359            LambdaExpr::Application {
1360                //John dances
1361                subformula: LambdaExprRef(2),
1362                argument: LambdaExprRef(4),
1363            },
1364            LambdaExpr::Lambda(LambdaExprRef(3), LambdaType::e().clone()),
1365            LambdaExpr::FreeVariable("0".into(), LambdaType::t().clone()),
1366            LambdaExpr::FreeVariable("2".into(), LambdaType::t().clone()),
1367            // 5
1368            //\lambda x. Mary sings and
1369            LambdaExpr::Application {
1370                subformula: LambdaExprRef(6),
1371                argument: LambdaExprRef(9),
1372            },
1373            LambdaExpr::Lambda(LambdaExprRef(7), LambdaType::t().clone()),
1374            LambdaExpr::Lambda(LambdaExprRef(8), LambdaType::t().clone()),
1375            LambdaExpr::BoundVariable(1, LambdaType::t().clone()),
1376            LambdaExpr::Application {
1377                //10
1378                subformula: LambdaExprRef(10),
1379                argument: LambdaExprRef(12),
1380            },
1381            LambdaExpr::Lambda(LambdaExprRef(11), LambdaType::e().clone()),
1382            LambdaExpr::FreeVariable("1337".into(), LambdaType::t().clone()),
1383            LambdaExpr::FreeVariable("5".into(), LambdaType::e().clone()),
1384        ]);
1385        pool.reduce(LambdaExprRef(0))?;
1386        pool.cleanup(LambdaExprRef(0));
1387        assert_eq!(
1388            pool,
1389            LambdaPool(vec![LambdaExpr::FreeVariable(
1390                "1337".into(),
1391                LambdaType::t().clone()
1392            )])
1393        );
1394        Ok(())
1395    }
1396
1397    #[test]
1398    fn test_lambda_calculus() -> anyhow::Result<()> {
1399        let mut pool = LambdaPool::<()>(
1400            k(0)?
1401                .into_iter()
1402                .chain([
1403                    LambdaExpr::FreeVariable("32".into(), LambdaType::e().clone()),
1404                    LambdaExpr::Application {
1405                        subformula: LambdaExprRef(0),
1406                        argument: LambdaExprRef(3),
1407                    },
1408                ])
1409                .collect(),
1410        );
1411        let root = LambdaExprRef(4);
1412        pool.beta_reduce(root)?;
1413        pool.cleanup(root);
1414
1415        assert_eq!(
1416            pool,
1417            LambdaPool(vec![
1418                LambdaExpr::FreeVariable("32".into(), LambdaType::e().clone()),
1419                LambdaExpr::Lambda(LambdaExprRef(0), LambdaType::e().clone())
1420            ])
1421        );
1422        Ok(())
1423    }
1424
1425    #[test]
1426    fn test_root_and_merger() -> anyhow::Result<()> {
1427        let man = RootedLambdaPool::parse("lambda a x (pa_man(x))")?;
1428
1429        let sleeps =
1430            RootedLambdaPool::parse("lambda a x (some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))")?;
1431        let every =
1432            RootedLambdaPool::parse("lambda <a,t> p (lambda <a,t> q every(x, p(x), q(x)))")?;
1433
1434        let phi = every.clone().merge(man.clone()).unwrap();
1435        let mut phi = phi.merge(sleeps.clone()).unwrap();
1436        println!("{phi}");
1437        phi.reduce()?;
1438        println!("{phi}");
1439        assert_eq!(
1440            phi,
1441            RootedLambdaPool::parse(
1442                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))"
1443            )?
1444        );
1445        assert!(check_hashes(
1446            &phi,
1447            &RootedLambdaPool::parse(
1448                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1449            )?,
1450        ));
1451        let pool = phi.into_pool()?;
1452        assert_eq!(
1453            "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1454            pool.to_string()
1455        );
1456        let phi = man.merge(every).unwrap();
1457        let mut phi = sleeps.merge(phi).unwrap();
1458        phi.reduce()?;
1459        assert_eq!(
1460            phi,
1461            RootedLambdaPool::parse(
1462                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1463            )?
1464        );
1465
1466        assert!(check_hashes(
1467            &phi,
1468            &RootedLambdaPool::parse(
1469                "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1470            )?,
1471        ));
1472
1473        let pool = phi.into_pool()?;
1474        assert_eq!(
1475            "every(x, pa_man(x), some_e(y, all_e, AgentOf(x, y) & pe_sleep(y)))",
1476            pool.to_string()
1477        );
1478        Ok(())
1479    }
1480
1481    fn check_hashes<'src>(
1482        phi: &RootedLambdaPool<'src, Expr<'src>>,
1483        psi: &RootedLambdaPool<'src, Expr<'src>>,
1484    ) -> bool {
1485        let mut hasher1 = DefaultHasher::new();
1486        let mut hasher2 = DefaultHasher::new();
1487
1488        phi.hash(&mut hasher1);
1489        psi.hash(&mut hasher2);
1490
1491        hasher1.finish() == hasher2.finish()
1492    }
1493
1494    #[test]
1495    fn bind_free_variable() -> anyhow::Result<()> {
1496        let mut pool = RootedLambdaPool::parse("phi#t & True")?;
1497
1498        pool.bind_free_variable("phi".into(), RootedLambdaPool::parse("False")?)?;
1499        assert_eq!("False & True", pool.into_pool()?.to_string());
1500
1501        let input = RootedLambdaPool::parse("lambda a x every_e(y,pe_4,AgentOf(x,y))")?;
1502        let mut a = RootedLambdaPool::parse("(P#<a,t>(a_3) & ~P#<a,t>(a_1))")?;
1503
1504        a.bind_free_variable("P".into(), input)?;
1505        a.reduce()?;
1506        assert_eq!(
1507            a.to_string(),
1508            "every_e(x, pe_4, AgentOf(a_3, x)) & ~every_e(x, pe_4, AgentOf(a_1, x))"
1509        );
1510        Ok(())
1511    }
1512
1513    #[test]
1514    fn apply_new_free_variable() -> anyhow::Result<()> {
1515        let mut pool =
1516            RootedLambdaPool::parse("lambda <e,t> P (lambda <e,t> Q (lambda e x (P(x) & Q(x))))")?;
1517
1518        pool.apply_new_free_variable("X".into())?;
1519
1520        let gold_pool = RootedLambdaPool {
1521            pool: LambdaPool(vec![
1522                LambdaExpr::FreeVariable("X".into(), LambdaType::et().clone()),
1523                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1524                LambdaExpr::Application {
1525                    subformula: LambdaExprRef(0),
1526                    argument: LambdaExprRef(1),
1527                },
1528                LambdaExpr::BoundVariable(1, LambdaType::et().clone()),
1529                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1530                LambdaExpr::Application {
1531                    subformula: LambdaExprRef(3),
1532                    argument: LambdaExprRef(4),
1533                },
1534                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(5))),
1535                LambdaExpr::Lambda(LambdaExprRef(6), LambdaType::e().clone()),
1536                LambdaExpr::Lambda(LambdaExprRef(7), LambdaType::et().clone()),
1537            ]),
1538            root: LambdaExprRef(8),
1539        };
1540        pool.cleanup();
1541        assert_eq!(pool, gold_pool);
1542        Ok(())
1543    }
1544
1545    #[test]
1546    fn lambda_abstraction() -> anyhow::Result<()> {
1547        let mut pool = RootedLambdaPool::parse(
1548            "lambda <e,t> P lambda <e,t> Q lambda e x Z#<e,t>(x) & P(x) & Q(x)",
1549        )?;
1550
1551        pool.lambda_abstract_free_variable("Z".into(), LambdaType::et().clone(), false)?;
1552
1553        let gold_pool = RootedLambdaPool {
1554            pool: LambdaPool(vec![
1555                LambdaExpr::BoundVariable(3, LambdaType::et().clone()),
1556                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1557                LambdaExpr::Application {
1558                    subformula: LambdaExprRef(0),
1559                    argument: LambdaExprRef(1),
1560                },
1561                LambdaExpr::BoundVariable(2, LambdaType::et().clone()),
1562                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1563                LambdaExpr::Application {
1564                    subformula: LambdaExprRef(3),
1565                    argument: LambdaExprRef(4),
1566                },
1567                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(2), ExprRef(5))),
1568                LambdaExpr::BoundVariable(1, LambdaType::et().clone()),
1569                LambdaExpr::BoundVariable(0, LambdaType::e().clone()),
1570                LambdaExpr::Application {
1571                    subformula: LambdaExprRef(7),
1572                    argument: LambdaExprRef(8),
1573                },
1574                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(6), ExprRef(9))),
1575                LambdaExpr::Lambda(LambdaExprRef(10), LambdaType::e().clone()),
1576                LambdaExpr::Lambda(LambdaExprRef(11), LambdaType::et().clone()),
1577                LambdaExpr::Lambda(LambdaExprRef(12), LambdaType::et().clone()),
1578                LambdaExpr::Lambda(LambdaExprRef(13), LambdaType::et().clone()),
1579            ]),
1580            root: LambdaExprRef(14),
1581        };
1582
1583        assert_eq!(pool, gold_pool);
1584        Ok(())
1585    }
1586
1587    #[test]
1588    fn could_time_out_if_swapping_instead_of_cloning() -> anyhow::Result<()> {
1589        let mut x = RootedLambdaPool::parse(
1590            "(lambda a x (PatientOf(x,e_0) & AgentOf(x, e_0)))((lambda a x (a_1))(a_0))",
1591        )?;
1592
1593        println!("{x}");
1594        x.reduce()?;
1595        println!("{x}");
1596        Ok(())
1597    }
1598
1599    #[test]
1600    fn lambda_abstraction_reduction() -> anyhow::Result<()> {
1601        let mut a = RootedLambdaPool::parse("a_1")?;
1602        let mut b = RootedLambdaPool::parse("(lambda t x (a_1))(pa_0(freeVar#a))")?;
1603
1604        a.lambda_abstract_free_variable("freeVar".into(), LambdaType::a().clone(), false)?;
1605        b.lambda_abstract_free_variable("freeVar".into(), LambdaType::a().clone(), false)?;
1606        println!("A:\t{a}");
1607        println!("B:\t{b}");
1608
1609        a.cleanup();
1610        b.cleanup();
1611        assert_eq!(a, b);
1612        Ok(())
1613    }
1614
1615    #[test]
1616    fn reduction_test() -> anyhow::Result<()> {
1617        let mut a = RootedLambdaPool::parse(
1618            "lambda a x (every_e(z, all_e, AgentOf(a_0, (lambda e y ((lambda e w (w))(y)))(z))))",
1619        )?;
1620        a.reduce()?;
1621
1622        let mut a = RootedLambdaPool::parse(
1623            "(lambda <a,t> P (P(a_3) & ~P(a_1)))(lambda a x (every_e(y,pe_4,AgentOf(x,y))))",
1624        )?;
1625
1626        a.pool.beta_reduce(a.root)?;
1627        a.root = a.pool.cleanup(a.root);
1628        println!("{a}");
1629        dbg!(&a);
1630
1631        let mut a = RootedLambdaPool::parse(
1632            "(lambda <a,t> P (P(a_3) & ~P(a_1)))(lambda a x (every_e(y,pe_4,AgentOf(x,y))))",
1633        )?;
1634
1635        a.reduce()?;
1636        assert_eq!(
1637            a.to_string(),
1638            "every_e(x, pe_4, AgentOf(a_3, x)) & ~every_e(x, pe_4, AgentOf(a_1, x))"
1639        );
1640
1641        Ok(())
1642    }
1643
1644    #[test]
1645    fn lift() -> anyhow::Result<()> {
1646        let mut e = RootedLambdaPool::parse("a_john")?;
1647        e.lift()?;
1648        assert_eq!(e.to_string(), "lambda <a,t> P P(a_john)");
1649
1650        Ok(())
1651    }
1652
1653    #[test]
1654    fn lambda_abstractions() -> anyhow::Result<()> {
1655        let mut e = RootedLambdaPool::parse(
1656            "(lambda t phi phi)(some_e(x, all_e, AgentOf(a_m, x) & PatientOf(blarg#a, x) & pe_likes(x)))",
1657        )?;
1658        e.reduce()?;
1659        e.lambda_abstract_free_variable(FreeVar::Named("blarg"), LambdaType::A, false)
1660            .unwrap();
1661        assert_eq!(
1662            e.to_string(),
1663            "lambda a x some_e(y, all_e, AgentOf(a_m, y) & PatientOf(x, y) & pe_likes(y))"
1664        );
1665        Ok(())
1666    }
1667
1668    #[test]
1669    fn is_constant_function() -> anyhow::Result<()> {
1670        let constants = [
1671            "lambda a x a_John",
1672            "lambda a x lambda a y pa_man(x)",
1673            "lambda a x some_e(y, all_e, pe_runs(y))",
1674        ];
1675        for s in constants {
1676            println!("{s}");
1677            let LambdaSummaryStats::WellFormed {
1678                lambda_type: _,
1679                constant_function,
1680                n_nodes: _,
1681            } = RootedLambdaPool::parse(s).unwrap().stats()
1682            else {
1683                panic!("{s} is poorly formed")
1684            };
1685            assert!(constant_function);
1686        }
1687
1688        let not_constants = [
1689            "lambda a x x",
1690            "lambda a x lambda a y pa_man(x) & pa_woman(y)",
1691        ];
1692        for s in not_constants {
1693            println!("{s}");
1694            let LambdaSummaryStats::WellFormed {
1695                lambda_type: _,
1696                constant_function,
1697                n_nodes: _,
1698            } = RootedLambdaPool::parse(s).unwrap().stats()
1699            else {
1700                panic!("{s} is poorly formed")
1701            };
1702            assert!(!constant_function);
1703        }
1704        Ok(())
1705    }
1706}
simple_semantics/lambda.rs

simple_semantics/
lambda.rs
