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: &[u32]) {
106        match self {
107            Expr::Quantifier {
108                restrictor,
109                subformula,
110                ..
111            } => {
112                *restrictor = ExprRef(remap[restrictor.0 as usize]);
113                *subformula = ExprRef(remap[subformula.0 as usize]);
114            }
115            Expr::Binary(_, x, y) => {
116                *x = ExprRef(remap[x.0 as usize]);
117                *y = ExprRef(remap[y.0 as usize]);
118            }
119            Expr::Unary(_, x) => {
120                *x = ExprRef(remap[x.0 as usize]);
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(u32::try_from(x).unwrap())))
175                }
176                LambdaExpr::BoundVariable(x, LambdaType::E) => {
177                    Ok(Expr::Variable(Variable::Event(u32::try_from(x).unwrap())))
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    fn cmp_expr(&self, other: &Self) -> std::cmp::Ordering {
212        self.ordering()
213            .cmp(&other.ordering())
214            .then_with(|| match (self, other) {
215                (
216                    Expr::Quantifier {
217                        quantifier,
218                        var_type,
219                        ..
220                    },
221                    Expr::Quantifier {
222                        quantifier: o_q,
223                        var_type: o_type,
224                        ..
225                    },
226                ) => var_type.cmp(o_type).then(quantifier.cmp(o_q)),
227                (Expr::Variable(x), Expr::Variable(y)) => x.cmp(y),
228                (Expr::Actor(x), Expr::Actor(y)) => x.cmp(y),
229                (Expr::Event(x), Expr::Event(y)) => x.cmp(y),
230                (Expr::Binary(x, ..), Expr::Binary(y, ..)) => x.cmp(y),
231                (Expr::Unary(x, _), Expr::Unary(y, _)) => x.cmp(y),
232                (Expr::Constant(x), Expr::Constant(y)) => x.cmp(y),
233                _ => panic!("Any non identical types already filtered"),
234            })
235    }
236}
237
238impl Expr<'_> {
239    fn ordering(&self) -> usize {
240        match self {
241            Expr::Quantifier { .. } => 0,
242            Expr::Variable(_) => 1,
243            Expr::Actor(_) => 2,
244            Expr::Event(_) => 3,
245            Expr::Binary(..) => 4,
246            Expr::Unary(..) => 5,
247            Expr::Constant(_) => 6,
248        }
249    }
250}
251
252impl HashLambda for Expr<'_> {
253    fn hash_expr<H: std::hash::Hasher>(&self, state: &mut H) {
254        match self {
255            Expr::Quantifier {
256                quantifier,
257                var_type,
258                ..
259            } => {
260                0.hash(state);
261                quantifier.hash(state);
262                var_type.hash(state);
263            }
264            Expr::Variable(variable) => {
265                1.hash(state);
266                variable.hash(state);
267            }
268            Expr::Actor(a) => {
269                2.hash(state);
270                a.hash(state);
271            }
272            Expr::Event(b) => {
273                3.hash(state);
274                b.hash(state);
275            }
276            Expr::Binary(bin_op, ..) => {
277                4.hash(state);
278                bin_op.hash(state);
279            }
280            Expr::Unary(mon_op, _) => {
281                5.hash(state);
282                mon_op.hash(state);
283            }
284            Expr::Constant(constant) => {
285                6.hash(state);
286                constant.hash(state);
287            }
288        }
289    }
290}
291
292impl<'a> std::fmt::Display for RootedLambdaPool<'a, Expr<'a>> {
293    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
294        let (string, _) = self.string(self.root(), VarContext::default(), false);
295        write!(f, "{string}")
296    }
297}
298
299static VARIABLENAMES: [&str; 26] = [
300    "x", "y", "z", "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m", "n", "o", "p",
301    "q", "r", "s", "t", "u", "v", "w",
302];
303
304static TRUTHS: [&str; 2] = ["phi", "psi"];
305
306static PREDICATENAMES: [&str; 3] = ["P", "Q", "R"];
307
308static OTHERFUNCTIONS: [&str; 4] = ["M", "N", "G", "K"];
309
310pub fn to_var(x: usize, t: Option<&LambdaType>) -> String {
311    let var_names = match t {
312        Some(t) if t == LambdaType::t() => TRUTHS.as_slice(),
313        Some(t) if t.is_one_place_function() => PREDICATENAMES.as_slice(),
314        Some(t) if t.is_function() => OTHERFUNCTIONS.as_slice(),
315        _ => VARIABLENAMES.as_slice(),
316    };
317
318    if x < var_names.len() {
319        var_names[x].to_string()
320    } else {
321        format!("{}{}", var_names[x % var_names.len()], x / var_names.len())
322    }
323}
324
325#[derive(Debug, Clone, Eq, PartialEq, Default)]
326pub(super) struct VarContext {
327    vars: HashMap<usize, usize>,
328    predicates: HashMap<usize, usize>,
329    other_functions: HashMap<usize, usize>,
330    truths: HashMap<usize, usize>,
331    depth: usize,
332}
333
334impl VarContext {
335    fn get_map(&self, t: Option<&LambdaType>) -> &HashMap<usize, usize> {
336        match t {
337            Some(t) if t == LambdaType::t() => &self.truths,
338            Some(t) if t.is_one_place_function() => &self.predicates,
339            Some(t) if t.is_function() => &self.other_functions,
340            _ => &self.vars,
341        }
342    }
343    fn get_map_mut(&mut self, t: Option<&LambdaType>) -> &mut HashMap<usize, usize> {
344        match t {
345            Some(t) if t == LambdaType::t() => &mut self.truths,
346            Some(t) if t.is_one_place_function() => &mut self.predicates,
347            Some(t) if t.is_function() => &mut self.other_functions,
348            _ => &mut self.vars,
349        }
350    }
351
352    pub(super) fn inc_depth_q(self, t: ActorOrEvent) -> (Self, String) {
353        let t: LambdaType = t.into();
354        self.inc_depth(&t)
355    }
356
357    pub(super) fn inc_depth(mut self, t: &LambdaType) -> (Self, String) {
358        let d = self.depth;
359        let map = self.get_map_mut(Some(t));
360        let n_var = map.len();
361        map.insert(d, n_var);
362        self.depth += 1;
363        (self, to_var(n_var, Some(t)))
364    }
365
366    pub(super) fn lambda_var(&self, bvar: usize, t: &LambdaType) -> String {
367        to_var(
368            *self.get_map(Some(t)).get(&(self.depth - bvar - 1)).unwrap(),
369            Some(t),
370        )
371    }
372}
373
374impl<'a> From<LanguageExpression<'a>> for RootedLambdaPool<'a, Expr<'a>> {
375    fn from(value: LanguageExpression<'a>) -> Self {
376        RootedLambdaPool {
377            pool: LambdaPool::from(
378                value
379                    .pool
380                    .0
381                    .iter()
382                    .map(|x| LambdaExpr::LanguageOfThoughtExpr(*x))
383                    .collect(),
384            ),
385            root: crate::lambda::LambdaExprRef(value.start.0),
386        }
387    }
388}
389
390#[derive(Debug, Copy, Clone, PartialEq, Eq)]
391pub(super) enum AssociativityData {
392    Lambda,
393    App,
394    Binom(BinOp),
395    Monop,
396}
397
398///An error which results from a failed application of [`RootedLambdaPool::conjoin`]
399#[derive(Debug, Clone, Error, PartialEq, Eq)]
400pub enum ConjoiningError {
401    ///Both arguments have to have the same type
402    #[error("Can't conjoin {0} and {1}")]
403    MismatchingTypes(LambdaType, LambdaType),
404
405    ///The type must return a truth value
406    #[error("Lambda type, {0} doesn't return a truth value")]
407    DoesntReturnT(LambdaType),
408
409    ///One of the arguments has an internal problem leading to reduction errors
410    #[error("One of the operands causes problems in reduction: {0})")]
411    ReductionError(#[from] ReductionError),
412}
413
414fn who_raises_who<'a>(
415    a: RootedLambdaPool<'a, Expr<'a>>,
416    b: RootedLambdaPool<'a, Expr<'a>>,
417) -> Result<
418    (
419        RootedLambdaPool<'a, Expr<'a>>,
420        RootedLambdaPool<'a, Expr<'a>>,
421    ),
422    ConjoiningError,
423> {
424    let a_type = a.get_type().unwrap();
425    let b_type = b.get_type().unwrap();
426
427    let Ok(a_rhs) = a_type.rhs() else {
428        return Err(ConjoiningError::DoesntReturnT(a_type));
429    };
430    let Ok(b_rhs) = b_type.rhs() else {
431        return Err(ConjoiningError::DoesntReturnT(b_type));
432    };
433    if b_rhs != &LambdaType::T && a_rhs != &LambdaType::T {
434        return Err(ConjoiningError::DoesntReturnT(a_type));
435    }
436
437    if a_rhs != &b_type && b_rhs != &a_type {
438        Err(ConjoiningError::MismatchingTypes(a_type, b_type))
439    } else if a_rhs == &b_type {
440        Ok((a, b))
441    } else {
442        Ok((b, a))
443    }
444}
445
446impl<'a> RootedLambdaPool<'a, Expr<'a>> {
447    ///Takes two lambda expressions, phi and psi of type <x, t> where x is any type and returns phi
448    ///AND psi.
449    ///
450    ///# Errors
451    ///Returns a [`ConjoiningError`] if `self` and `other` are not of the right types such that a
452    //conjoining can happen.
453    #[allow(clippy::missing_panics_doc)]
454    pub fn conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
455        let self_type = self.get_type().unwrap();
456        let other_type = other.get_type().unwrap();
457        if self_type != other_type {
458            return Err(ConjoiningError::MismatchingTypes(self_type, other_type));
459        }
460
461        let Ok((lhs, rhs)) = self_type.split() else {
462            return Err(ConjoiningError::DoesntReturnT(self_type));
463        };
464
465        if rhs != &LambdaType::T {
466            return Err(ConjoiningError::DoesntReturnT(self_type));
467        }
468        let lhs = lhs.clone();
469
470        let combinator = RootedLambdaPool {
471            pool: LambdaPool(vec![
472                LambdaExpr::Lambda(LambdaExprRef(1), self_type.clone()),
473                LambdaExpr::Lambda(LambdaExprRef(2), other_type.clone()),
474                LambdaExpr::Lambda(LambdaExprRef(3), lhs.clone()),
475                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(BinOp::And, ExprRef(4), ExprRef(7))),
476                LambdaExpr::Application {
477                    subformula: LambdaExprRef(5),
478                    argument: LambdaExprRef(6),
479                },
480                LambdaExpr::BoundVariable(2, self_type),
481                LambdaExpr::BoundVariable(0, lhs.clone()),
482                LambdaExpr::Application {
483                    subformula: LambdaExprRef(8),
484                    argument: LambdaExprRef(9),
485                },
486                LambdaExpr::BoundVariable(1, other_type),
487                LambdaExpr::BoundVariable(0, lhs),
488            ]),
489            root: LambdaExprRef(0),
490        };
491
492        let mut conjoined = combinator.merge(self).unwrap().merge(other).unwrap();
493        conjoined.reduce()?;
494        Ok(conjoined)
495    }
496
497    ///Takes two lambda expressions, phi <x, <y,t>> and psi of type <y, t> where x and y is any type and returns phi
498    ///AND psi.
499    ///
500    ///This is a generalized kind of Event Identification from Kratzer (1996)
501    ///
502    /// - 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>
503    ///
504    ///# Errors
505    ///Returns a [`ConjoiningError`] if `self` and `other` are not of the right types such that a
506    //raised conjoining can happen.
507    #[allow(clippy::missing_panics_doc)]
508    pub fn raised_conjoin(self, other: Self) -> Result<Self, ConjoiningError> {
509        let (a, b) = who_raises_who(self, other)?;
510        let a_type = a.get_type().unwrap();
511        let b_type = b.get_type().unwrap();
512
513        let Ok(event) = a_type.lhs() else {
514            return Err(ConjoiningError::DoesntReturnT(a_type));
515        };
516
517        let Ok(e) = b_type.lhs() else {
518            return Err(ConjoiningError::DoesntReturnT(b_type));
519        };
520        let e = e.clone();
521        let event = event.clone();
522
523        let combinator = RootedLambdaPool {
524            pool: LambdaPool(vec![
525                LambdaExpr::Lambda(LambdaExprRef(1), a_type.clone()),
526                LambdaExpr::Lambda(LambdaExprRef(2), b_type.clone()),
527                LambdaExpr::Lambda(LambdaExprRef(3), event.clone()),
528                LambdaExpr::Lambda(LambdaExprRef(4), e.clone()),
529                LambdaExpr::LanguageOfThoughtExpr(Expr::Binary(
530                    BinOp::And,
531                    ExprRef(5),
532                    ExprRef(10),
533                )),
534                LambdaExpr::Application {
535                    subformula: LambdaExprRef(6),
536                    argument: LambdaExprRef(9),
537                },
538                LambdaExpr::Application {
539                    subformula: LambdaExprRef(7),
540                    argument: LambdaExprRef(8),
541                },
542                LambdaExpr::BoundVariable(3, a_type),
543                LambdaExpr::BoundVariable(1, event),
544                LambdaExpr::BoundVariable(0, e.clone()),
545                LambdaExpr::Application {
546                    subformula: LambdaExprRef(11),
547                    argument: LambdaExprRef(12),
548                },
549                LambdaExpr::BoundVariable(2, b_type),
550                LambdaExpr::BoundVariable(0, e),
551            ]),
552            root: LambdaExprRef(0),
553        };
554
555        let mut conjoined = combinator.merge(a).unwrap().merge(b).unwrap();
556        conjoined.reduce()?;
557        Ok(conjoined)
558    }
559
560    ///Create a [`RootedLambdaPool<Expr>`] from a string.
561    ///
562    ///# Errors
563    ///Returns a [`LambdaParseError`] if the input string is malformed and not a LOT expression.
564    pub fn parse(s: &'a str) -> Result<Self, LambdaParseError> {
565        parse_lot(s)
566    }
567
568    #[allow(clippy::too_many_lines)]
569    fn string(
570        &self,
571        expr: LambdaExprRef,
572        c: VarContext,
573        parent_is_app: bool,
574    ) -> (String, AssociativityData) {
575        match self.get(expr) {
576            LambdaExpr::Lambda(child, lambda_type) => {
577                let (c, var) = c.inc_depth(lambda_type);
578                (
579                    format!(
580                        "lambda {} {} {}",
581                        lambda_type,
582                        var,
583                        self.string(*child, c, false).0
584                    ),
585                    AssociativityData::Lambda,
586                )
587            }
588            LambdaExpr::Application {
589                subformula,
590                argument,
591            } => {
592                let (sub, associative) = self.string(*subformula, c.clone(), true);
593                let (arg, _) = self.string(*argument, c, false); // false
594                // since apps only collapse if they're a left chain
595
596                let mut s = match associative {
597                    AssociativityData::Lambda | AssociativityData::Binom(_) => {
598                        format!("({sub})({arg}")
599                    }
600                    AssociativityData::Monop => format!("{sub}({arg}"),
601                    AssociativityData::App => format!("{sub}{arg}"),
602                };
603
604                if parent_is_app {
605                    s.push_str(", ");
606                } else {
607                    s.push(')');
608                }
609
610                (s, AssociativityData::App)
611            }
612            LambdaExpr::BoundVariable(bvar, lambda_type) => {
613                (c.lambda_var(*bvar, lambda_type), AssociativityData::Monop)
614            }
615            LambdaExpr::FreeVariable(fvar, t) => (format!("{fvar}#{t}"), AssociativityData::Monop),
616            LambdaExpr::LanguageOfThoughtExpr(x) => match x {
617                Expr::Variable(variable) => (
618                    c.lambda_var(variable.id() as usize, variable.as_lambda_type()),
619                    AssociativityData::Monop,
620                ),
621                Expr::Quantifier {
622                    quantifier,
623                    var_type,
624                    restrictor,
625                    subformula,
626                } => {
627                    let (c, var_string) = c.inc_depth_q(*var_type);
628                    let (restrictor, _) =
629                        self.string(LambdaExprRef(restrictor.0), c.clone(), false);
630                    let (subformula, _) = self.string(LambdaExprRef(subformula.0), c, false);
631                    (
632                        format!(
633                            "{}{}({}, {restrictor}, {subformula})",
634                            quantifier,
635                            match var_type {
636                                ActorOrEvent::Actor => "",
637                                ActorOrEvent::Event => "_e",
638                            },
639                            var_string,
640                        ),
641                        AssociativityData::Monop,
642                    )
643                }
644                Expr::Unary(MonOp::Iota(var_type), arg) => {
645                    let (c, var_string) = c.inc_depth_q(*var_type);
646                    let (arg, _) = self.string(LambdaExprRef(arg.0), c, false);
647                    (
648                        format!(
649                            "iota{}({}, {arg})",
650                            match var_type {
651                                ActorOrEvent::Actor => "",
652                                ActorOrEvent::Event => "_e",
653                            },
654                            var_string,
655                        ),
656                        AssociativityData::Monop,
657                    )
658                }
659                Expr::Actor(a) => (format!("a_{a}"), AssociativityData::Monop),
660                Expr::Event(e) => (format!("e_{e}"), AssociativityData::Monop),
661                Expr::Binary(bin_op, x, y) => {
662                    let (x, x_a) = self.string(LambdaExprRef(x.0), c.clone(), false);
663                    let (y, y_a) = self.string(LambdaExprRef(y.0), c, false);
664                    match bin_op {
665                        BinOp::AgentOf | BinOp::PatientOf => {
666                            (format!("{bin_op}({x}, {y})",), AssociativityData::Monop)
667                        }
668
669                        BinOp::And | BinOp::Or => (
670                            {
671                                let mut s = String::default();
672                                if add_parenthesis_for_bin_op(*bin_op, x_a) {
673                                    write!(s, "({x})").unwrap();
674                                } else {
675                                    s.push_str(&x);
676                                }
677                                write!(s, " {bin_op} ").unwrap();
678                                if add_parenthesis_for_bin_op(*bin_op, y_a) {
679                                    write!(s, "({y})").unwrap();
680                                } else {
681                                    s.push_str(&y);
682                                }
683                                s
684                            },
685                            AssociativityData::Binom(*bin_op),
686                        ),
687                    }
688                }
689                Expr::Unary(mon_op, arg) => {
690                    let (arg, arg_binom) = self.string(LambdaExprRef(arg.0), c, false);
691                    (
692                        match mon_op {
693                            MonOp::Not => match arg_binom {
694                                AssociativityData::Binom(BinOp::And | BinOp::Or) => {
695                                    format!("{mon_op}({arg})")
696                                }
697                                AssociativityData::Binom(_)
698                                | AssociativityData::Lambda
699                                | AssociativityData::App
700                                | AssociativityData::Monop => {
701                                    format!("{mon_op}{arg}")
702                                }
703                            },
704                            _ => format!("{mon_op}({arg})"),
705                        },
706                        AssociativityData::Monop,
707                    )
708                }
709                Expr::Constant(constant) => (format!("{constant}"), AssociativityData::Monop),
710            },
711        }
712    }
713}
714
715pub(super) fn add_parenthesis_for_bin_op(x: BinOp, data: AssociativityData) -> bool {
716    match data {
717        AssociativityData::Binom(b) => match b {
718            BinOp::AgentOf | BinOp::PatientOf => false,
719            BinOp::And | BinOp::Or if b == x => false,
720            BinOp::And | BinOp::Or => true,
721        },
722        AssociativityData::Lambda => true,
723        AssociativityData::App | AssociativityData::Monop => false,
724    }
725}
726
727#[cfg(test)]
728mod test {
729    use super::to_var;
730
731    use crate::lambda::{FreeVar, types::LambdaType};
732    use crate::{Entity, Scenario, ThetaRoles, lambda::RootedLambdaPool, parse_executable};
733
734    #[test]
735    fn fancy_printing() -> anyhow::Result<()> {
736        for statement in [
737            "~AgentOf(a_John, e_0)",
738            "pa_Red(a_John) & ~pa_Red(a_Mary)",
739            "every(x, all_a, pa_Blue(x))",
740            "every(x, pa_Blue, pa_Blue(x))",
741            "every(x, pa_5, pa_10(a_59))",
742            "every_e(x, all_e, PatientOf(a_Mary, x))",
743        ] {
744            println!("{statement}");
745            let expression = parse_executable(statement)?;
746            assert_eq!(expression.to_string(), statement);
747        }
748        for s in [
749            "cool#<a,t>(a_John)",
750            "bad#<a,t>(man#a)",
751            "woah#<<e,t>,t>(lambda e x pe_wow(x))",
752            "lambda <a,t> P lambda a x P(x)",
753            "lambda <a,t> P P(a_man) & ~P(a_woman)",
754            "loves#<a,<a,t>>(a_john, a_mary)",
755            "gives#<a,<a,<a,t>>>(a_john, a_mary, a_present)",
756            "lambda e x lambda a y loves#<e,<a,t>>(x, y)",
757        ] {
758            println!("{s}");
759            let p = RootedLambdaPool::parse(s)?;
760            assert_eq!(p.to_string(), s);
761        }
762
763        Ok(())
764    }
765
766    #[test]
767    fn type_checking() -> anyhow::Result<()> {
768        let john = RootedLambdaPool::parse("a_John")?;
769        let likes = RootedLambdaPool::parse(
770            "lambda a x ((lambda a y (some_e(e, all_e, AgentOf(x, e) & PatientOf(y, e) & pe_likes(e)))))",
771        )?;
772
773        let mary = RootedLambdaPool::parse("a_Mary")?;
774        let phi = mary.clone().merge(likes.clone()).unwrap();
775        let mut phi = phi.merge(john.clone()).unwrap();
776        phi.reduce()?;
777        let pool = phi.into_pool()?;
778        assert_eq!(
779            "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
780            pool.to_string()
781        );
782        let phi = likes.merge(mary).unwrap();
783        let mut phi = john.merge(phi).unwrap();
784        phi.reduce()?;
785        let pool = phi.into_pool()?;
786        assert_eq!(
787            "some_e(x, all_e, AgentOf(a_Mary, x) & PatientOf(a_John, x) & pe_likes(x))",
788            pool.to_string()
789        );
790        Ok(())
791    }
792
793    #[test]
794    fn var_name_assigner() {
795        assert_eq!(to_var(0, None), "x");
796        assert_eq!(to_var(1, None), "y");
797        assert_eq!(to_var(2, None), "z");
798        assert_eq!(to_var(26, None), "x1");
799        assert_eq!(to_var(27, None), "y1");
800        assert_eq!(to_var(28, None), "z1");
801        assert_eq!(to_var(26 * 300, None), "x300");
802    }
803
804    #[test]
805    fn printing() -> anyhow::Result<()> {
806        let pool = RootedLambdaPool::parse(
807            "some_e(x0, all_e, AgentOf(a_1, x0) & PatientOf(a_0, x0) & pe_0(x0))",
808        )?;
809        assert_eq!(
810            pool.to_string(),
811            "some_e(x, all_e, AgentOf(a_1, x) & PatientOf(a_0, x) & pe_0(x))"
812        );
813        let likes = RootedLambdaPool::parse(
814            "lambda e x lambda e y (some(e, all_a, AgentOf(e, x) & PatientOf(e, y) & pe_likes(y)))",
815        )?;
816
817        let s =
818            "lambda e x lambda e y some(z, all_a, AgentOf(z, x) & PatientOf(z, y) & pe_likes(y))";
819        assert_eq!(likes.to_string(), s,);
820        let likes2 = RootedLambdaPool::parse(s)?;
821        assert_eq!(likes, likes2);
822
823        Ok(())
824    }
825
826    #[test]
827    fn fancy_quantification_reduction() -> anyhow::Result<()> {
828        let pool = RootedLambdaPool::parse("every_e(x0,pe_0(x0) & pe_1(x0), pe_2(x0))")?;
829        let scenario = Scenario::new(
830            vec![],
831            vec![ThetaRoles::default(); 5],
832            [
833                ("0", vec![Entity::Event(1), Entity::Event(2)]),
834                ("1", vec![Entity::Event(0), Entity::Event(1)]),
835                ("2", vec![Entity::Event(1)]),
836            ]
837            .into_iter()
838            .collect(),
839        );
840
841        dbg!(&pool);
842        assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
843
844        let pool = RootedLambdaPool::parse("every_e(x0, pe_0(x0) & pe_1(x0), pe_2(x0))")?;
845
846        let scenario = Scenario::new(
847            vec![],
848            vec![ThetaRoles::default(); 5],
849            [
850                ("0", vec![Entity::Event(1), Entity::Event(2)]),
851                ("1", vec![Entity::Event(0), Entity::Event(1)]),
852                ("2", vec![Entity::Event(1)]),
853            ]
854            .into_iter()
855            .collect(),
856        );
857
858        dbg!(&pool);
859        assert!(pool.into_pool()?.run(&scenario, None)?.try_into()?);
860
861        let pool =
862            RootedLambdaPool::parse("every_e(x, pe_laughs, every(y, pe_sleeps(x), pa_woman(y)))")?;
863        println!("{}", pool.into_pool()?);
864        Ok(())
865    }
866
867    #[test]
868    fn conjoining_check() -> anyhow::Result<()> {
869        let tall = RootedLambdaPool::parse("lambda a x pa_tall(x)")?;
870        let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
871
872        let mut tall_man = tall.conjoin(man)?;
873        tall_man.reduce()?;
874        let weird = RootedLambdaPool::parse("weird#<a,t>")?;
875        let man = RootedLambdaPool::parse("lambda a x pa_man(x)")?;
876        let weird_man = weird.conjoin(man)?;
877        assert_eq!(format!("{tall_man}"), "lambda a x pa_tall(x) & pa_man(x)");
878        assert_eq!(
879            format!("{weird_man}"),
880            "lambda a x weird#<a,t>(x) & pa_man(x)"
881        );
882
883        let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
884        let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
885
886        let mut agent_run = voice.raised_conjoin(run)?;
887        agent_run.reduce()?;
888        assert_eq!(
889            format!("{agent_run}"),
890            "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
891        );
892        let voice = RootedLambdaPool::parse("lambda a x lambda e y AgentOf(x, y)")?;
893        let run = RootedLambdaPool::parse("lambda e x pe_run(x)")?;
894
895        let mut agent_run = run.raised_conjoin(voice)?;
896        agent_run.reduce()?;
897        assert_eq!(
898            format!("{agent_run}"),
899            "lambda a x lambda e y AgentOf(x, y) & pe_run(y)"
900        );
901        Ok(())
902    }
903
904    #[test]
905    fn alpha_check() -> anyhow::Result<()> {
906        let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
907        let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
908        let mut likes = RootedLambdaPool::parse(
909            "lambda a x (lambda a y (some_e(e, all_e, AgentOf(y, e)&pe_likes(e)&PatientOf(x, e))))",
910        )?;
911
912        likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
913        let mut sentence = likes.merge(someone).unwrap();
914        sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
915        let mut sentence = sentence.merge(everyone).unwrap();
916        sentence.reduce()?;
917
918        assert_eq!(
919            sentence.to_string(),
920            "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z))))"
921        );
922
923        assert_eq!(
924            sentence,
925            RootedLambdaPool::parse(
926                "every(x, all_a, some(y, all_a, some_e(z, all_e, AgentOf(y, z) & pe_likes(z) & PatientOf(x, z))))"
927            )?
928        );
929
930        let everyone = RootedLambdaPool::parse("lambda <a,t> P (every(x, all_a, P(x)))")?;
931        let someone = RootedLambdaPool::parse("lambda <a,t> P (some(x, all_a, P(x)))")?;
932        let mut likes = RootedLambdaPool::parse(
933            "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)))))",
934        )?;
935
936        likes.apply_new_free_variable(FreeVar::Anonymous(0))?;
937        let mut sentence = likes.merge(someone).unwrap();
938        sentence.lambda_abstract_free_variable(FreeVar::Anonymous(0), LambdaType::A, true)?;
939        let mut sentence = sentence.merge(everyone).unwrap();
940        sentence.reduce()?;
941        assert_eq!(
942            sentence,
943            RootedLambdaPool::parse(
944                "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)))))"
945            )?
946        );
947        Ok(())
948    }
949}
simple_semantics/language/lambda_implementation.rs

simple_semantics/language/
lambda_implementation.rs
