simple_semantics/language/
lambda_implementation.rs

1use crate::{lambda::HashLambda, utils::ArgumentIterator};
2use ahash::HashMap;
3use std::{fmt::Write, hash::Hash, iter::empty};
4use thiserror::Error;
5
6use super::{
7    ActorOrEvent, BinOp, Constant, Expr, ExprPool, ExprRef, LambdaParseError, LanguageExpression,
8    MonOp, Variable,
9};
10use crate::{
11    lambda::{
12        LambdaExpr, LambdaExprRef, LambdaLanguageOfThought, LambdaPool, ReductionError,
13        RootedLambdaPool, types::LambdaType,
14    },
15    language::parser::parse_lot,
16};
17
18impl From<ExprRef> for LambdaExprRef {
19    fn from(value: ExprRef) -> Self {
20        LambdaExprRef(value.0)
21    }
22}
23
24impl From<LambdaExprRef> for ExprRef {
25    fn from(value: LambdaExprRef) -> Self {
26        ExprRef(value.0)
27    }
28}
29
30#[derive(Debug, Clone, Error, PartialEq, Eq)]
31pub enum LambdaConversionError {
32    #[error("There are still lambda terms in this pool")]
33    StillHasLambdaTerms,
34    #[error("Reducing lambda exprs in quantifiers is leading to a bug ({0})")]
35    ReductionError(#[from] ReductionError),
36}
37
38impl<'a> LambdaLanguageOfThought for Expr<'a> {
39    type Pool = LanguageExpression<'a>;
40    type ConversionError = LambdaConversionError;
41
42    fn n_children(&self) -> usize {
43        match self {
44            Expr::Quantifier { .. } | Expr::Binary(..) => 2,
45            Expr::Unary(..) => 1,
46            Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => 0,
47        }
48    }
49
50    fn inc_depth(&self) -> bool {
51        matches!(
52            self,
53            Expr::Quantifier { .. } | Expr::Unary(MonOp::Iota(_), _)
54        )
55    }
56
57    fn var_type(&self) -> Option<&LambdaType> {
58        match self {
59            Expr::Quantifier { var_type, .. } | Expr::Unary(MonOp::Iota(var_type), _) => {
60                match var_type {
61                    ActorOrEvent::Actor => Some(LambdaType::a()),
62                    ActorOrEvent::Event => Some(LambdaType::e()),
63                }
64            }
65            _ => None,
66        }
67    }
68
69    fn get_children(&self) -> impl Iterator<Item = LambdaExprRef> {
70        match self {
71            Expr::Quantifier {
72                restrictor,
73                subformula,
74                ..
75            } => vec![restrictor, subformula],
76            Expr::Binary(_, x, y) => vec![x, y],
77            Expr::Unary(_, x) => vec![x],
78            Expr::Constant(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Variable(_) => vec![],
79        }
80        .into_iter()
81        .map(|x| LambdaExprRef(x.0))
82    }
83
84    fn change_children(&mut self, mut new_children: impl Iterator<Item = LambdaExprRef>) {
85        match self {
86            Expr::Quantifier {
87                restrictor,
88                subformula,
89                ..
90            } => {
91                *restrictor = ExprRef(new_children.next().unwrap().0);
92                *subformula = ExprRef(new_children.next().unwrap().0);
93            }
94            Expr::Binary(_, x, y) => {
95                *x = ExprRef(new_children.next().unwrap().0);
96                *y = ExprRef(new_children.next().unwrap().0);
97            }
98            Expr::Unary(_, x) => {
99                *x = ExprRef(new_children.next().unwrap().0);
100            }
101            Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => (),
102        }
103    }
104
105    fn remap_refs(&mut self, remap: &[usize]) {
106        match self {
107            Expr::Quantifier {
108                restrictor,
109                subformula,
110                ..
111            } => {
112                *restrictor = ExprRef(remap[restrictor.0 as usize] as u32);
113                *subformula = ExprRef(remap[subformula.0 as usize] as u32);
114            }
115            Expr::Binary(_, x, y) => {
116                *x = ExprRef(remap[x.0 as usize] as u32);
117                *y = ExprRef(remap[y.0 as usize] as u32);
118            }
119            Expr::Unary(_, x) => {
120                *x = ExprRef(remap[x.0 as usize] as u32);
121            }
122            Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => (),
123        }
124    }
125
126    fn get_type(&self) -> &LambdaType {
127        match self {
128            Expr::Quantifier { .. } => LambdaType::t(),
129            Expr::Variable(Variable::Actor(_)) | Expr::Actor(_) => LambdaType::a(),
130            Expr::Variable(Variable::Event(_)) | Expr::Event(_) => LambdaType::e(),
131            Expr::Binary(bin, ..) => match bin {
132                BinOp::AgentOf | BinOp::PatientOf | BinOp::And | BinOp::Or => LambdaType::t(),
133            },
134            Expr::Unary(mon_op, _) => match mon_op {
135                MonOp::Property(_, _) | MonOp::Not => LambdaType::t(),
136                MonOp::Iota(ActorOrEvent::Actor) => LambdaType::a(),
137                MonOp::Iota(ActorOrEvent::Event) => LambdaType::e(),
138            },
139            Expr::Constant(constant) => match constant {
140                Constant::Everyone | Constant::Property(_, ActorOrEvent::Actor) => LambdaType::at(),
141                Constant::EveryEvent | Constant::Property(_, ActorOrEvent::Event) => {
142                    LambdaType::et()
143                }
144                Constant::Contradiction | Constant::Tautology => LambdaType::t(),
145            },
146        }
147    }
148
149    fn same_expr(&self, other: &Self) -> bool {
150        match self {
151            Expr::Quantifier {
152                quantifier: q1,
153                var_type: v1,
154                ..
155            } => {
156                matches!(other, Expr::Quantifier{ quantifier: q2, var_type: v2, .. } if q1==q2 && v1==v2)
157            }
158            Expr::Variable(_) | Expr::Actor(_) | Expr::Event(_) | Expr::Constant(_) => {
159                self == other
160            }
161            Expr::Binary(b1, ..) => matches!(other, Expr::Binary(b2, ..) if b1==b2),
162            Expr::Unary(m1, _) => matches!(other, Expr::Unary(m2,_) if m1==m2),
163        }
164    }
165
166    fn to_pool(pool: RootedLambdaPool<Self>) -> Result<Self::Pool, Self::ConversionError> {
167        let processed_pool = pool
168            .pool
169            .0
170            .into_iter()
171            .map(|x| match x {
172                LambdaExpr::LanguageOfThoughtExpr(x) => Ok(x),
173                LambdaExpr::BoundVariable(x, LambdaType::A) => {
174                    Ok(Expr::Variable(Variable::Actor(x as u32)))
175                }
176                LambdaExpr::BoundVariable(x, LambdaType::E) => {
177                    Ok(Expr::Variable(Variable::Event(x as u32)))
178                }
179                _ => Err(LambdaConversionError::StillHasLambdaTerms),
180            })
181            .collect::<Result<Vec<_>, LambdaConversionError>>()?;
182
183        Ok(LanguageExpression {
184            pool: ExprPool(processed_pool),
185            start: ExprRef(pool.root.0),
186        })
187    }
188
189    fn get_arguments(&self) -> impl Iterator<Item = LambdaType> {
190        match self {
191            Expr::Quantifier { .. } => {
192                ArgumentIterator::A([LambdaType::t().clone(), LambdaType::t().clone()].into_iter())
193            }
194            Expr::Binary(b, _, _) => {
195                ArgumentIterator::B(b.get_argument_type().into_iter().cloned())
196            }
197            Expr::Unary(mon_op, _) => {
198                ArgumentIterator::C([mon_op.get_argument_type().clone()].into_iter())
199            }
200            Expr::Variable(Variable::Event(_) | Variable::Actor(_))
201            | Expr::Actor(_)
202            | Expr::Event(_)
203            | Expr::Constant(_) => ArgumentIterator::D(empty()),
204        }
205    }
206
207    fn commutative(&self) -> bool {
208        matches!(self, Expr::Binary(BinOp::And | BinOp::Or, ..))
209    }
210}
211
212impl HashLambda for Expr<'_> {
213    fn hash_expr<H: std::hash::Hasher>(&self, state: &mut H) {
214        match self {
215            Expr::Quantifier {
216                quantifier,
217                var_type,
218                ..
219            } => {
220                0.hash(state);
221                quantifier.hash(state);
222                var_type.hash(state);
223            }
224            Expr::Variable(variable) => {
225                1.hash(state);
226                variable.hash(state);
227            }
228            Expr::Actor(a) => {
229                2.hash(state);
230                a.hash(state);
231            }
232            Expr::Event(b) => {
233                3.hash(state);
234                b.hash(state);
235            }
236            Expr::Binary(bin_op, ..) => {
237                4.hash(state);
238                bin_op.hash(state);
239            }
240            Expr::Unary(mon_op, _) => {
241                5.hash(state);
242                mon_op.hash(state);
243            }
244            Expr::Constant(constant) => {
245                6.hash(state);
246                constant.hash(state);
247            }
248        }
249    }
250}
251
252impl<'a> std::fmt::Display for RootedLambdaPool<'a, Expr<'a>> {
253    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
254        let (string, _) = self.string(self.root(), VarContext::default(), false);
255        write!(f, "{string}")
256    }
257}
258
259static VARIABLENAMES: [&str; 26] = [
260    "x", "y", "z", "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p",
261    "q", "r", "s", "t", "u", "v", "w",
262];
263
264static TRUTHS: [&str; 2] = ["phi", "psi"];
265
266static PREDICATENAMES: [&str; 3] = ["P", "Q", "R"];
267
268static OTHERFUNCTIONS: [&str; 4] = ["M", "N", "G", "K"];
269
270pub fn to_var(x: usize, t: Option<&LambdaType>) -> String {
271    let var_names = match t {
272        Some(t) if t == LambdaType::t() => TRUTHS.as_slice(),
273        Some(t) if t.is_one_place_function() => PREDICATENAMES.as_slice(),
274        Some(t) if t.is_function() => OTHERFUNCTIONS.as_slice(),
275        _ => VARIABLENAMES.as_slice(),
276    };
277
278    if x < var_names.len() {
279        var_names[x].to_string()
280    } else {
281        format!("{}{}", var_names[x % var_names.len()], x / var_names.len())
282    }
283}
284
285#[derive(Debug, Clone, Eq, PartialEq, Default)]
286pub(super) struct VarContext {
287    vars: HashMap<usize, usize>,
288    predicates: HashMap<usize, usize>,
289    other_functions: HashMap<usize, usize>,
290    truths: HashMap<usize, usize>,
291    depth: usize,
292}
293
294impl VarContext {
295    fn get_map(&self, t: Option<&LambdaType>) -> &HashMap<usize, usize> {
296        match t {
297            Some(t) if t == LambdaType::t() => &self.truths,
298            Some(t) if t.is_one_place_function() => &self.predicates,
299            Some(t) if t.is_function() => &self.other_functions,
300            _ => &self.vars,
301        }
302    }
303    fn get_map_mut(&mut self, t: Option<&LambdaType>) -> &mut HashMap<usize, usize> {
304        match t {
305            Some(t) if t == LambdaType::t() => &mut self.truths,
306            Some(t) if t.is_one_place_function() => &mut self.predicates,
307            Some(t) if t.is_function() => &mut self.other_functions,
308            _ => &mut self.vars,
309        }
310    }
311
312    pub(super) fn inc_depth_q(self, t: ActorOrEvent) -> (Self, String) {
313        let t: LambdaType = t.into();
314        self.inc_depth(&t)
315    }
316
317    pub(super) fn inc_depth(mut self, t: &LambdaType) -> (Self, String) {
318        let d = self.depth;
319        let map = self.get_map_mut(Some(t));
320        let n_var = map.len();
321        map.insert(d, n_var);
322        self.depth += 1;
323        (self, to_var(n_var, Some(t)))
324    }
325
326    pub(super) fn lambda_var(&self, bvar: usize, t: &LambdaType) -> String {
327        to_var(
328            *self.get_map(Some(t)).get(&(self.depth - bvar - 1)).unwrap(),
329            Some(t),
330        )
331    }
332}
333
334impl<'a> From<LanguageExpression<'a>> for RootedLambdaPool<'a, Expr<'a>> {
335    fn from(value: LanguageExpression<'a>) -> Self {
336        RootedLambdaPool {
337            pool: LambdaPool::from(
338                value
339                    .pool
340                    .0
341                    .iter()
342                    .map(|x| LambdaExpr::LanguageOfThoughtExpr(*x))
343                    .collect(),
344            ),
345            root: crate::lambda::LambdaExprRef(value.start.0),
346        }
347    }
348}
349
350#[derive(Debug, Copy, Clone, PartialEq, Eq)]
351pub(super) enum AssociativityData {
352    Lambda,
353    App,
354    Binom(BinOp),
355    Monop,
356}
357
358///An error which results from a failed application of [`RootedLambdaPool::conjoin`]
359#[derive(Debug, Clone, Error, PartialEq, Eq)]
360pub enum ConjoiningError {
361    ///Both arguments have to have the same type
362    #[error("Can't conjoin {0} and {1}")]
363    MismatchingTypes(LambdaType, LambdaType),
364
365    ///The type must return a truth value
366    #[error("Lambda type, {0} doesn't return a truth value")]
367    DoesntReturnT(LambdaType),
368
369    ///One of the arguments has an internal problem leading to reduction errors
370    #[error("One of the operands causes problems in reduction: {0})")]
371    ReductionError(#[from] ReductionError),
372}
373
374fn who_raises_who<'a>(
375    a: RootedLambdaPool<'a, Expr<'a>>,
376    b: RootedLambdaPool<'a, Expr<'a>>,
377) -> Result<
378    (
379        RootedLambdaPool<'a, Expr<'a>>,
380        RootedLambdaPool<'a, Expr<'a>>,
381    ),
382    ConjoiningError,
383> {
384    let a_type = a.get_type().unwrap();
385    let b_type = b.get_type().unwrap();
386
387    let Ok(a_rhs) = a_type.rhs() else {
388        return Err(ConjoiningError::DoesntReturnT(a_type));
389    };
390    let Ok(b_rhs) = b_type.rhs() else {
391        return Err(ConjoiningError::DoesntReturnT(b_type));
392    };
393    if b_rhs != &LambdaType::T && a_rhs != &LambdaType::T {
394        return Err(ConjoiningError::DoesntReturnT(a_type));
395    }
396
397    if a_rhs != &b_type && b_rhs != &a_type {
398        Err(ConjoiningError::MismatchingTypes(a_type, b_type))
399    } else if a_rhs == &b_type {
400        Ok((a, b))
401    } else {
402        Ok((b, a))
403    }
404}
405
406impl<'a> RootedLambdaPool<'a, Expr<'a>> {
407    ///Takes two lambda expressions, phi and psi of type <x, t> where x is any type and returns phi
408    ///AND psi.
409    pub fn conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
410        let self_type = self.get_type().unwrap();
411        let other_type = other.get_type().unwrap();
412        if self_type != other_type {
413            return Err(ConjoiningError::MismatchingTypes(self_type, other_type));
414        }
415
416        let Ok((lhs, rhs)) = self_type.split() else {
417            return Err(ConjoiningError::DoesntReturnT(self_type));
418        };
419
420        if rhs != &LambdaType::T {
421            return Err(ConjoiningError::DoesntReturnT(self_type));
422        }
423        let lhs = lhs.clone();
424
425        let combinator = RootedLambdaPool {
426            pool: LambdaPool(vec![
427                LambdaExpr::Lambda(LambdaExprRef(1), self_type.clone()),
428                LambdaExpr::Lambda(LambdaExprRef(2), other_type.clone()),
429                LambdaExpr::Lambda(LambdaExprRef(3), lhs.clone()),
430                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(4), ExprRef(7))),
431                LambdaExpr::Application {
432                    subformula: LambdaExprRef(5),
433                    argument: LambdaExprRef(6),
434                },
435                LambdaExpr::BoundVariable(2, self_type),
436                LambdaExpr::BoundVariable(0, lhs.clone()),
437                LambdaExpr::Application {
438                    subformula: LambdaExprRef(8),
439                    argument: LambdaExprRef(9),
440                },
441                LambdaExpr::BoundVariable(1, other_type),
442                LambdaExpr::BoundVariable(0, lhs),
443            ]),
444            root: LambdaExprRef(0),
445        };
446
447        let mut conjoined = combinator.merge(self).unwrap().merge(other).unwrap();
448        conjoined.reduce()?;
449        Ok(conjoined)
450    }
451
452    ///Takes two lambda expressions, phi <x, <y,t>> and psi of type <y, t> where x and y is any type and returns phi
453    ///AND psi.
454    ///
455    ///This is a generalized kind of Event Identification from Kratzer (1996)
456    ///
457    /// - Kratzer, A. (1996). Severing the External Argument from its Verb. In J. Rooryck & L. Zaring (Eds.), Phrase Structure and the Lexicon (pp. 109–137). Springer Netherlands. <https://doi.org/10.1007/978-94-015-8617-7_5>
458    pub fn raised_conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
459        let (a, b) = who_raises_who(self, other)?;
460        let a_type = a.get_type().unwrap();
461        let b_type = b.get_type().unwrap();
462
463        let Ok(event) = a_type.lhs() else {
464            return Err(ConjoiningError::DoesntReturnT(a_type));
465        };
466
467        let Ok(e) = b_type.lhs() else {
468            return Err(ConjoiningError::DoesntReturnT(b_type));
469        };
470        let e = e.clone();
471        let event = event.clone();
472
473        let combinator = RootedLambdaPool {
474            pool: LambdaPool(vec![
475                LambdaExpr::Lambda(LambdaExprRef(1), a_type.clone()),
476                LambdaExpr::Lambda(LambdaExprRef(2), b_type.clone()),
477                LambdaExpr::Lambda(LambdaExprRef(3), event.clone()),
478                LambdaExpr::Lambda(LambdaExprRef(4), e.clone()),
479                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(
480                    BinOp::And,
481                    ExprRef(5),
482                    ExprRef(10),
483                )),
484                LambdaExpr::Application {
485                    subformula: LambdaExprRef(6),
486                    argument: LambdaExprRef(9),
487                },
488                LambdaExpr::Application {
489                    subformula: LambdaExprRef(7),
490                    argument: LambdaExprRef(8),
491                },
492                LambdaExpr::BoundVariable(3, a_type),
493                LambdaExpr::BoundVariable(1, event),
494                LambdaExpr::BoundVariable(0, e.clone()),
495                LambdaExpr::Application {
496                    subformula: LambdaExprRef(11),
497                    argument: LambdaExprRef(12),
498                },
499                LambdaExpr::BoundVariable(2, b_type),
500                LambdaExpr::BoundVariable(0, e),
501            ]),
502            root: LambdaExprRef(0),
503        };
504
505        let mut conjoined = combinator.merge(a).unwrap().merge(b).unwrap();
506        conjoined.reduce()?;
507        Ok(conjoined)
508    }
509
510    ///Create a [`RootedLambdaPool<Expr>`] from a string.
511    pub fn parse(s: &'a str) -> Result<Self, LambdaParseError> {
512        parse_lot(s)
513    }
514
515    fn string(
516        &self,
517        expr: LambdaExprRef,
518        c: VarContext,
519        parent_is_app: bool,
520    ) -> (String, AssociativityData) {
521        match self.get(expr) {
522            LambdaExpr::Lambda(child, lambda_type) => {
523                let (c, var) = c.inc_depth(lambda_type);
524                (
525                    format!(
526                        "lambda {} {} {}",
527                        lambda_type,
528                        var,
529                        self.string(*child, c, false).0
530                    ),
531                    AssociativityData::Lambda,
532                )
533            }
534            LambdaExpr::Application {
535                subformula,
536                argument,
537            } => {
538                let (sub, associative) = self.string(*subformula, c.clone(), true);
539                let (arg, _) = self.string(*argument, c, false); // false
540                // since apps only collapse if they're a left chain
541
542                let mut s = match associative {
543                    AssociativityData::Lambda | AssociativityData::Binom(_) => {
544                        format!("({sub})({arg}")
545                    }
546                    AssociativityData::Monop => format!("{sub}({arg}"),
547                    AssociativityData::App => format!("{sub}{arg}"),
548                };
549
550                if parent_is_app {
551                    s.push_str(", ");
552                } else {
553                    s.push(')');
554                }
555
556                (s, AssociativityData::App)
557            }
558            LambdaExpr::BoundVariable(bvar, lambda_type) => {
559                (c.lambda_var(*bvar, lambda_type), AssociativityData::Monop)
560            }
561            LambdaExpr::FreeVariable(fvar, t) => (format!("{fvar}#{t}"), AssociativityData::Monop),
562            LambdaExpr::LanguageOfThoughtExpr(x) => match x {
563                Expr::Variable(variable) => (
564                    c.lambda_var(variable.id() as usize, variable.as_lambda_type()),
565                    AssociativityData::Monop,
566                ),
567                Expr::Quantifier {
568                    quantifier,
569                    var_type,
570                    restrictor,
571                    subformula,
572                } => {
573                    let (c, var_string) = c.inc_depth_q(*var_type);
574                    let (restrictor, _) =
575                        self.string(LambdaExprRef(restrictor.0), c.clone(), false);
576                    let (subformula, _) = self.string(LambdaExprRef(subformula.0), c, false);
577                    (
578                        format!(
579                            "{}{}({}, {restrictor}, {subformula})",
580                            quantifier,
581                            match var_type {
582                                ActorOrEvent::Actor => "",
583                                ActorOrEvent::Event => "_e",
584                            },
585                            var_string,
586                        ),
587                        AssociativityData::Monop,
588                    )
589                }
590                Expr::Unary(MonOp::Iota(var_type), arg) => {
591                    let (c, var_string) = c.inc_depth_q(*var_type);
592                    let (arg, _) = self.string(LambdaExprRef(arg.0), c, false);
593                    (
594                        format!(
595                            "iota{}({}, {arg})",
596                            match var_type {
597                                ActorOrEvent::Actor => "",
598                                ActorOrEvent::Event => "_e",
599                            },
600                            var_string,
601                        ),
602                        AssociativityData::Monop,
603                    )
604                }
605                Expr::Actor(a) => (format!("a_{a}"), AssociativityData::Monop),
606                Expr::Event(e) => (format!("e_{e}"), AssociativityData::Monop),
607                Expr::Binary(bin_op, x, y) => {
608                    let (x, x_a) = self.string(LambdaExprRef(x.0), c.clone(), false);
609                    let (y, y_a) = self.string(LambdaExprRef(y.0), c, false);
610                    match bin_op {
611                        BinOp::AgentOf | BinOp::PatientOf => {
612                            (format!("{bin_op}({x}, {y})",), AssociativityData::Monop)
613                        }
614
615                        BinOp::And | BinOp::Or => (
616                            {
617                                let mut s = String::default();
618                                if add_parenthesis_for_bin_op(*bin_op, x_a) {
619                                    write!(s, "({x})").unwrap();
620                                } else {
621                                    s.push_str(&x);
622                                }
623                                write!(s, " {bin_op} ").unwrap();
624                                if add_parenthesis_for_bin_op(*bin_op, y_a) {
625                                    write!(s, "({y})").unwrap();
626                                } else {
627                                    s.push_str(&y);
628                                }
629                                s
630                            },
631                            AssociativityData::Binom(*bin_op),
632                        ),
633                    }
634                }
635                Expr::Unary(mon_op, arg) => {
636                    let (arg, arg_binom) = self.string(LambdaExprRef(arg.0), c, false);
637                    (
638                        match mon_op {
639                            MonOp::Not => match arg_binom {
640                                AssociativityData::Binom(BinOp::And | BinOp::Or) => {
641                                    format!("{mon_op}({arg})")
642                                }
643                                AssociativityData::Binom(_)
644                                | AssociativityData::Lambda
645                                | AssociativityData::App
646                                | AssociativityData::Monop => {
647                                    format!("{mon_op}{arg}")
648                                }
649                            },
650                            _ => format!("{mon_op}({arg})"),
651                        },
652                        AssociativityData::Monop,
653                    )
654                }
655                Expr::Constant(constant) => (format!("{constant}"), AssociativityData::Monop),
656            },
657        }
658    }
659}
660
661pub(super) fn add_parenthesis_for_bin_op(x: BinOp, data: AssociativityData) -> bool {
662    match data {
663        AssociativityData::Binom(b) => match b {
664            BinOp::AgentOf | BinOp::PatientOf => false,
665            BinOp::And | BinOp::Or if b == x => false,
666            BinOp::And | BinOp::Or => true,
667        },
668        AssociativityData::Lambda => true,
669        AssociativityData::App | AssociativityData::Monop => false,
670    }
671}
672
673#[cfg(test)]
674mod test {
675    use super::to_var;
676
677    use crate::lambda::{FreeVar, types::LambdaType};
678    use crate::{Entity, Scenario, ThetaRoles, lambda::RootedLambdaPool, parse_executable};
679
680    #[test]
681    fn fancy_printing() -> anyhow::Result<()> {
682        for statement in [
683            "~AgentOf(a_John, e_0)",
684            "pa_Red(a_John) & ~pa_Red(a_Mary)",
685            "every(x, all_a, pa_Blue(x))",
686            "every(x, pa_Blue, pa_Blue(x))",
687            "every(x, pa_5, pa_10(a_59))",
688            "every_e(x, all_e, PatientOf(a_Mary, x))",
689        ] {
690            println!("{statement}");
691            let expression = parse_executable(statement)?;
692            assert_eq!(expression.to_string(), statement);
693        }
694        for s in [
695            "cool#<a,t>(a_John)",
696            "bad#<a,t>(man#a)",
697            "woah#<<e,t>,t>(lambda e x pe_wow(x))",
698            "lambda <a,t> P lambda a x P(x)",
699            "lambda <a,t> P P(a_man) & ~P(a_woman)",
700            "loves#<a,<a,t>>(a_john, a_mary)",
701            "gives#<a,<a,<a,t>>>(a_john, a_mary, a_present)",
702            "lambda e x lambda a y loves#<e,<a,t>>(x, y)",
703        ] {
704            println!("{s}");
705            let p = RootedLambdaPool::parse(s)?;
706            assert_eq!(p.to_string(), s);
707        }
708
709        Ok(())
710    }
711
712    #[test]
713    fn type_checking() -> anyhow::Result<()> {
714        let john = RootedLambdaPool::parse("a_John")?;
715        let likes = RootedLambdaPool::parse(
716            "lambda a x ((lambda a y (some_e(e, all_e, AgentOf(x, e) & PatientOf(y, e) & pe_likes(e)))))",
717        )?;
718
719        let mary = RootedLambdaPool::parse("a_Mary")?;
720        let phi = mary.clone().merge(likes.clone()).unwrap();
721        let mut phi = phi.merge(john.clone()).unwrap();
722        phi.reduce()?;
723        let pool = phi.into_pool()?;
724        assert_eq!(
725            "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
726            pool.to_string()
727        );
728        let phi = likes.merge(mary).unwrap();
729        let mut phi = john.merge(phi).unwrap();
730        phi.reduce()?;
731        let pool = phi.into_pool()?;
732        assert_eq!(
733            "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
734            pool.to_string()
735        );
736        Ok(())
737    }
738
739    #[test]
740    fn var_name_assigner() {
741        assert_eq!(to_var(0, None), "x");
742        assert_eq!(to_var(1, None), "y");
743        assert_eq!(to_var(2, None), "z");
744        assert_eq!(to_var(26, None), "x1");
745        assert_eq!(to_var(27, None), "y1");
746        assert_eq!(to_var(28, None), "z1");
747        assert_eq!(to_var(26 * 300, None), "x300");
748    }
749
750    #[test]
751    fn printing() -> anyhow::Result<()> {
752        let pool = RootedLambdaPool::parse(
753            "some_e(x0, all_e, AgentOf(a_1, x0) & PatientOf(a_0, x0) & pe_0(x0))",
754        )?;
755        assert_eq!(
756            pool.to_string(),
757            "some_e(x, all_e, AgentOf(a_1, x) & PatientOf(a_0, x) & pe_0(x))"
758        );
759        let likes = RootedLambdaPool::parse(
760            "lambda e x lambda e y (some(e, all_a, AgentOf(e, x) & PatientOf(e, y) & pe_likes(y)))",
761        )?;
762
763        let s =
764            "lambda e x lambda e y some(z, all_a, AgentOf(z, x) & PatientOf(z, y) & pe_likes(y))";
765        assert_eq!(likes.to_string(), s,);
766        let likes2 = RootedLambdaPool::parse(s)?;
767        assert_eq!(likes, likes2);
768
769        Ok(())
770    }
771
772    #[test]
773    fn fancy_quantification_reduction() -> anyhow::Result<()> {
774        let pool = RootedLambdaPool::parse("every_e(x0,pe_0(x0) & pe_1(x0), pe_2(x0))")?;
775        let scenario = Scenario::new(
776            vec![],
777            vec![ThetaRoles::default(); 5],
778            [
779                ("0", vec![Entity::Event(1), Entity::Event(2)]),
780                ("1", vec![Entity::Event(0), Entity::Event(1)]),
781                ("2", vec![Entity::Event(1)]),
782            ]
783            .into_iter()
784            .collect(),
785        );
786
787        dbg!(&pool);
788        assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
789
790        let pool = RootedLambdaPool::parse("every_e(x0, pe_0(x0) & pe_1(x0), pe_2(x0))")?;
791
792        let scenario = Scenario::new(
793            vec![],
794            vec![ThetaRoles::default(); 5],
795            [
796                ("0", vec![Entity::Event(1), Entity::Event(2)]),
797                ("1", vec![Entity::Event(0), Entity::Event(1)]),
798                ("2", vec![Entity::Event(1)]),
799            ]
800            .into_iter()
801            .collect(),
802        );
803
804        dbg!(&pool);
805        assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
806
807        let pool =
808            RootedLambdaPool::parse("every_e(x, pe_laughs, every(y, pe_sleeps(x), pa_woman(y)))")?;
809        println!("{}", pool.into_pool()?);
810        Ok(())
811    }
812
813    #[test]
814    fn conjoining_check() -> anyhow::Result<()> {
815        let tall = RootedLambdaPool::parse("lambda a x pa_tall(x)")?;
816        let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
817
818        let mut tall_man = tall.conjoin(man)?;
819        tall_man.reduce()?;
820        let weird = RootedLambdaPool::parse("weird#<a,t>")?;
821        let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
822        let weird_man = weird.conjoin(man)?;
823        assert_eq!(format!("{tall_man}"), "lambda a x pa_tall(x) & pa_man(x)");
824        assert_eq!(
825            format!("{weird_man}"),
826            "lambda a x weird#<a,t>(x) & pa_man(x)"
827        );
828
829        let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
830        let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
831
832        let mut agent_run = voice.raised_conjoin(run)?;
833        agent_run.reduce()?;
834        assert_eq!(
835            format!("{agent_run}"),
836            "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
837        );
838        let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
839        let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
840
841        let mut agent_run = run.raised_conjoin(voice)?;
842        agent_run.reduce()?;
843        assert_eq!(
844            format!("{agent_run}"),
845            "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
846        );
847        Ok(())
848    }
849
850    #[test]
851    fn alpha_check() -> anyhow::Result<()> {
852        let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
853        let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
854        let mut likes = RootedLambdaPool::parse(
855            "lambda a x (lambda a y (some_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e))))",
856        )?;
857
858        likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
859        let mut sentence = likes.merge(someone).unwrap();
860        sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
861        let mut sentence = sentence.merge(everyone).unwrap();
862        sentence.reduce()?;
863
864        assert_eq!(
865            sentence.to_string(),
866            "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z))))"
867        );
868
869        assert_eq!(
870            sentence,
871            RootedLambdaPool::parse(
872                "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z))))"
873            )?
874        );
875
876        let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
877        let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
878        let mut likes = RootedLambdaPool::parse(
879            "lambda a x (lambda a y ( some_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e)) | some(w, all_a, every_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e)))))",
880        )?;
881
882        likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
883        let mut sentence = likes.merge(someone).unwrap();
884        sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
885        let mut sentence = sentence.merge(everyone).unwrap();
886        sentence.reduce()?;
887        assert_eq!(
888            sentence,
889            RootedLambdaPool::parse(
890                "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z)) | some(z, all_a, every_e(a, all_e, AgentOf(y, a) & pe_likes(a) & PatientOf(x, a)))))"
891            )?
892        );
893        Ok(())
894    }
895}
simple_semantics/language/lambda_implementation.rs

simple_semantics/language/
lambda_implementation.rs
