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

simple_semantics/
lambda.rs
