logicaffeine_language/
lambda.rs

1//! Lambda calculus transformations for Montague-style compositional semantics.
2//!
3//! This module provides functions for manipulating logical expressions using
4//! lambda abstraction and application. It supports:
5//!
6//! - **Quantifier raising** via type-lifting (proper names → generalized quantifiers)
7//! - **Beta reduction** for applying lambda abstractions
8//! - **Scope enumeration** to generate all possible quantifier scopings
9//! - **Intensional contexts** for opaque verbs (believes, seeks, wants)
10//! - **Event semantics** transformation (Davidson-style)
11//!
12//! # Key Functions
13//!
14//! | Function | Purpose |
15//! |----------|---------|
16//! | [`lift_proper_name`] | Lifts a proper name to a generalized quantifier |
17//! | [`lift_quantifier`] | Creates a quantifier lambda term |
18//! | [`beta_reduce`] | Performs beta reduction on applications |
19//! | [`enumerate_scopings`] | Generates all scope permutations respecting islands |
20//! | [`enumerate_intensional_readings`] | Generates de re / de dicto readings |
21//! | [`to_event_semantics`] | Converts predicate to neo-Davidsonian event form |
22//!
23//! # Scope Islands
24//!
25//! Quantifiers are assigned an `island_id` during parsing. The scoping algorithm
26//! only permutes quantifiers within the same island. This prevents:
27//! - Wh-extraction from relative clauses
28//! - Quantifier raising out of adjuncts
29//! - Other island constraint violations
30//!
31//! # Intensionality
32//!
33//! Opaque verbs create intensional contexts where substitution of co-referential
34//! terms may change truth value. The module provides:
35//! - `make_intensional`: Wraps an expression in an intensional operator
36//! - `substitute_respecting_opacity`: Blocks substitution inside intensional contexts
37
38use logicaffeine_base::Arena;
39use crate::ast::{LogicExpr, QuantifierKind, Term};
40use logicaffeine_base::{Interner, Symbol};
41use crate::lexicon;
42use crate::token::TokenType;
43
44fn clone_term<'a>(term: &Term<'a>, arena: &'a Arena<Term<'a>>) -> Term<'a> {
45    match term {
46        Term::Constant(s) => Term::Constant(*s),
47        Term::Variable(s) => Term::Variable(*s),
48        Term::Function(name, args) => {
49            let cloned_args: Vec<Term<'a>> = args.iter().map(|t| clone_term(t, arena)).collect();
50            Term::Function(*name, arena.alloc_slice(cloned_args))
51        }
52        Term::Group(members) => {
53            let cloned: Vec<Term<'a>> = members.iter().map(|t| clone_term(t, arena)).collect();
54            Term::Group(arena.alloc_slice(cloned))
55        }
56        Term::Possessed { possessor, possessed } => Term::Possessed {
57            possessor: arena.alloc(clone_term(possessor, arena)),
58            possessed: *possessed,
59        },
60        Term::Sigma(predicate) => Term::Sigma(*predicate),
61        Term::Intension(predicate) => Term::Intension(*predicate),
62        Term::Proposition(expr) => Term::Proposition(*expr),
63        Term::Value { kind, unit, dimension } => Term::Value {
64            kind: *kind,
65            unit: *unit,
66            dimension: *dimension,
67        },
68    }
69}
70
71/// Checks if a verb creates an opaque (intensional) context.
72///
73/// Opaque verbs like "believes", "wants", "seeks" block substitution
74/// of co-referential terms. For example:
75/// - "John believes Clark Kent flies" ≠ "John believes Superman flies"
76pub fn is_opaque_verb(verb: Symbol, interner: &Interner) -> bool {
77    let verb_str = interner.resolve(verb);
78    let lower = verb_str.to_lowercase();
79    lexicon::is_opaque_verb(&lower)
80}
81
82/// Wraps an expression in an intensional operator.
83///
84/// Creates `operator[content]` for de dicto readings of intensional verbs.
85pub fn make_intensional<'a>(
86    operator: Symbol,
87    content: &'a LogicExpr<'a>,
88    arena: &'a Arena<LogicExpr<'a>>,
89) -> &'a LogicExpr<'a> {
90    arena.alloc(LogicExpr::Intensional { operator, content })
91}
92
93/// Substitutes a variable with a replacement, respecting opacity boundaries.
94///
95/// Unlike standard substitution, this function does NOT substitute inside
96/// intensional contexts, preserving the opacity of verbs like "believes".
97pub fn substitute_respecting_opacity<'a>(
98    expr: &'a LogicExpr<'a>,
99    var: Symbol,
100    replacement: &'a LogicExpr<'a>,
101    expr_arena: &'a Arena<LogicExpr<'a>>,
102    term_arena: &'a Arena<Term<'a>>,
103) -> &'a LogicExpr<'a> {
104    match expr {
105        LogicExpr::Intensional { operator, content } => {
106            expr_arena.alloc(LogicExpr::Intensional {
107                operator: *operator,
108                content: *content,
109            })
110        }
111
112        LogicExpr::Predicate { name, args, .. } => {
113            let new_args: Vec<Term<'a>> = args
114                .iter()
115                .map(|arg| substitute_term_for_opacity(arg, var, replacement, term_arena))
116                .collect();
117            expr_arena.alloc(LogicExpr::Predicate {
118                name: *name,
119                args: term_arena.alloc_slice(new_args),
120                world: None,
121            })
122        }
123
124        LogicExpr::BinaryOp { left, op, right } => expr_arena.alloc(LogicExpr::BinaryOp {
125            left: substitute_respecting_opacity(left, var, replacement, expr_arena, term_arena),
126            op: op.clone(),
127            right: substitute_respecting_opacity(right, var, replacement, expr_arena, term_arena),
128        }),
129
130        LogicExpr::UnaryOp { op, operand } => expr_arena.alloc(LogicExpr::UnaryOp {
131            op: op.clone(),
132            operand: substitute_respecting_opacity(operand, var, replacement, expr_arena, term_arena),
133        }),
134
135        LogicExpr::Quantifier { kind, variable, body, island_id } => {
136            if *variable == var {
137                expr
138            } else {
139                expr_arena.alloc(LogicExpr::Quantifier {
140                    kind: *kind,
141                    variable: *variable,
142                    body: substitute_respecting_opacity(body, var, replacement, expr_arena, term_arena),
143                    island_id: *island_id,
144                })
145            }
146        }
147
148        LogicExpr::Lambda { variable, body } => {
149            if *variable == var {
150                expr
151            } else {
152                expr_arena.alloc(LogicExpr::Lambda {
153                    variable: *variable,
154                    body: substitute_respecting_opacity(body, var, replacement, expr_arena, term_arena),
155                })
156            }
157        }
158
159        LogicExpr::App { function, argument } => expr_arena.alloc(LogicExpr::App {
160            function: substitute_respecting_opacity(function, var, replacement, expr_arena, term_arena),
161            argument: substitute_respecting_opacity(argument, var, replacement, expr_arena, term_arena),
162        }),
163
164        LogicExpr::Atom(s) => {
165            if *s == var {
166                replacement
167            } else {
168                expr
169            }
170        }
171
172        _ => expr,
173    }
174}
175
176fn substitute_term_for_opacity<'a>(
177    term: &Term<'a>,
178    var: Symbol,
179    replacement: &LogicExpr<'a>,
180    arena: &'a Arena<Term<'a>>,
181) -> Term<'a> {
182    match term {
183        Term::Constant(c) if *c == var => {
184            match replacement {
185                LogicExpr::Atom(s) => Term::Constant(*s),
186                _ => clone_term(term, arena),
187            }
188        }
189        Term::Variable(v) if *v == var => {
190            match replacement {
191                LogicExpr::Atom(s) => Term::Constant(*s),
192                _ => clone_term(term, arena),
193            }
194        }
195        _ => clone_term(term, arena),
196    }
197}
198
199/// Converts a predicate to Neo-Davidsonian event semantics.
200///
201/// Transforms `P(x, y)` into `∃e(P(e) ∧ Agent(e, x) ∧ Theme(e, y))`.
202/// This reification of events enables reasoning about event modification.
203pub fn to_event_semantics<'a>(
204    expr: &'a LogicExpr<'a>,
205    interner: &mut Interner,
206    expr_arena: &'a Arena<LogicExpr<'a>>,
207    term_arena: &'a Arena<Term<'a>>,
208) -> &'a LogicExpr<'a> {
209    match expr {
210        LogicExpr::Predicate { name, args, .. } => {
211            let e_sym = interner.intern("e");
212            let _event_var = term_arena.alloc(Term::Variable(e_sym));
213
214            let event_pred = expr_arena.alloc(LogicExpr::Predicate {
215                name: *name,
216                args: term_arena.alloc_slice([Term::Variable(e_sym)]),
217                world: None,
218            });
219
220            let mut body = event_pred;
221
222            if !args.is_empty() {
223                let agent_args = term_arena.alloc_slice([Term::Variable(e_sym), clone_term(&args[0], term_arena)]);
224                let agent_pred = expr_arena.alloc(LogicExpr::Predicate {
225                    name: interner.intern("Agent"),
226                    args: agent_args,
227                    world: None,
228                });
229                body = expr_arena.alloc(LogicExpr::BinaryOp {
230                    left: body,
231                    op: TokenType::And,
232                    right: agent_pred,
233                });
234            }
235
236            if args.len() > 1 {
237                let theme_args = term_arena.alloc_slice([Term::Variable(e_sym), clone_term(&args[1], term_arena)]);
238                let theme_pred = expr_arena.alloc(LogicExpr::Predicate {
239                    name: interner.intern("Theme"),
240                    args: theme_args,
241                    world: None,
242                });
243                body = expr_arena.alloc(LogicExpr::BinaryOp {
244                    left: body,
245                    op: TokenType::And,
246                    right: theme_pred,
247                });
248            }
249
250            if args.len() > 2 {
251                let goal_args = term_arena.alloc_slice([Term::Variable(e_sym), clone_term(&args[2], term_arena)]);
252                let goal_pred = expr_arena.alloc(LogicExpr::Predicate {
253                    name: interner.intern("Goal"),
254                    args: goal_args,
255                    world: None,
256                });
257                body = expr_arena.alloc(LogicExpr::BinaryOp {
258                    left: body,
259                    op: TokenType::And,
260                    right: goal_pred,
261                });
262            }
263
264            expr_arena.alloc(LogicExpr::Quantifier {
265                kind: QuantifierKind::Existential,
266                variable: e_sym,
267                body,
268                island_id: 0,
269            })
270        }
271        _ => expr,
272    }
273}
274
275/// Adds an adverbial modifier to an event.
276///
277/// Transforms `∃e(P(e) ∧ ...)` into `∃e(P(e) ∧ Adverb(e) ∧ ...)`.
278pub fn apply_adverb<'a>(
279    expr: &'a LogicExpr<'a>,
280    adverb: Symbol,
281    interner: &mut Interner,
282    expr_arena: &'a Arena<LogicExpr<'a>>,
283    term_arena: &'a Arena<Term<'a>>,
284) -> &'a LogicExpr<'a> {
285    let e_sym = interner.intern("e");
286    match expr {
287        LogicExpr::Quantifier { kind, variable, body, island_id } if *variable == e_sym => {
288            let adverb_str = interner.resolve(adverb);
289            let capitalized = capitalize(adverb_str);
290            let adverb_pred = expr_arena.alloc(LogicExpr::Predicate {
291                name: interner.intern(&capitalized),
292                args: term_arena.alloc_slice([Term::Variable(*variable)]),
293                world: None,
294            });
295
296            let new_body = expr_arena.alloc(LogicExpr::BinaryOp {
297                left: *body,
298                op: TokenType::And,
299                right: adverb_pred,
300            });
301
302            expr_arena.alloc(LogicExpr::Quantifier {
303                kind: *kind,
304                variable: *variable,
305                body: new_body,
306                island_id: *island_id,
307            })
308        }
309        _ => expr,
310    }
311}
312
313fn capitalize(s: &str) -> String {
314    let mut chars = s.chars();
315    match chars.next() {
316        None => String::new(),
317        Some(first) => first.to_uppercase().collect::<String>() + chars.as_str(),
318    }
319}
320
321fn factorial(n: usize) -> u64 {
322    (1..=n as u64).product()
323}
324
325pub struct ScopeIterator<'a> {
326    expr_arena: &'a Arena<LogicExpr<'a>>,
327    islands: Vec<Vec<ScopalElement<'a>>>,
328    core: &'a LogicExpr<'a>,
329    current_index: u64,
330    total: u64,
331    single_result: Option<&'a LogicExpr<'a>>,
332    returned_single: bool,
333}
334
335impl<'a> ScopeIterator<'a> {
336    fn nth_island_aware_permutation(&self, n: u64) -> Vec<ScopalElement<'a>> {
337        let mut result = Vec::new();
338        let mut remainder = n;
339
340        for island in &self.islands {
341            let island_perms = factorial(island.len());
342            let island_index = remainder % island_perms;
343            remainder /= island_perms;
344
345            let perm = nth_permutation_of_slice(island, island_index);
346            result.extend(perm);
347        }
348
349        result
350    }
351}
352
353fn nth_permutation_of_slice<T: Clone>(items: &[T], n: u64) -> Vec<T> {
354    let len = items.len();
355    let mut available: Vec<usize> = (0..len).collect();
356    let mut result = Vec::with_capacity(len);
357    let mut remainder = n;
358
359    for i in 0..len {
360        let divisor = factorial(len - i - 1);
361        let index = (remainder / divisor) as usize;
362        remainder %= divisor;
363        result.push(items[available.remove(index)].clone());
364    }
365    result
366}
367
368impl<'a> Iterator for ScopeIterator<'a> {
369    type Item = &'a LogicExpr<'a>;
370
371    fn next(&mut self) -> Option<Self::Item> {
372        if let Some(single) = self.single_result {
373            if self.returned_single {
374                return None;
375            }
376            self.returned_single = true;
377            return Some(single);
378        }
379
380        if self.current_index >= self.total {
381            return None;
382        }
383        let ordered = self.nth_island_aware_permutation(self.current_index);
384        self.current_index += 1;
385        Some(rebuild_with_scopal_elements(&ordered, self.core, self.expr_arena))
386    }
387
388    fn size_hint(&self) -> (usize, Option<usize>) {
389        if self.single_result.is_some() {
390            let remaining = if self.returned_single { 0 } else { 1 };
391            return (remaining, Some(remaining));
392        }
393        let remaining = (self.total - self.current_index) as usize;
394        (remaining, Some(remaining))
395    }
396}
397
398impl<'a> ExactSizeIterator for ScopeIterator<'a> {}
399
400#[derive(Clone, Debug)]
401struct QuantifierInfo<'a> {
402    kind: QuantifierKind,
403    variable: Symbol,
404    restrictor: &'a LogicExpr<'a>,
405    island_id: u32,
406}
407
408#[derive(Clone, Debug)]
409enum ScopalElement<'a> {
410    Quantifier(QuantifierInfo<'a>),
411    Negation { island_id: u32 },
412}
413
414impl<'a> ScopalElement<'a> {
415    fn island_id(&self) -> u32 {
416        match self {
417            ScopalElement::Quantifier(q) => q.island_id,
418            ScopalElement::Negation { island_id } => *island_id,
419        }
420    }
421}
422
423/// Generates all possible quantifier scopings for an expression.
424///
425/// Returns an iterator over all scope-permuted versions of the expression,
426/// respecting scope island constraints. Quantifiers with the same `island_id`
427/// can be permuted; quantifiers in different islands maintain relative order.
428///
429/// # Example
430///
431/// "Every man loves a woman" has two readings:
432/// - Surface scope: ∀x(Man(x) → ∃y(Woman(y) ∧ Love(x,y)))
433/// - Inverse scope: ∃y(Woman(y) ∧ ∀x(Man(x) → Love(x,y)))
434pub fn enumerate_scopings<'a>(
435    expr: &'a LogicExpr<'a>,
436    interner: &mut Interner,
437    expr_arena: &'a Arena<LogicExpr<'a>>,
438    _term_arena: &'a Arena<Term<'a>>,
439) -> ScopeIterator<'a> {
440    let mut elements = Vec::new();
441    let core = extract_scopal_elements(expr, &mut elements, interner, expr_arena);
442
443    if elements.is_empty() || elements.len() == 1 {
444        return ScopeIterator {
445            expr_arena,
446            islands: Vec::new(),
447            core,
448            current_index: 0,
449            total: 0,
450            single_result: Some(expr),
451            returned_single: false,
452        };
453    }
454
455    let islands = group_scopal_by_island(elements);
456    let total: u64 = islands.iter().map(|island| factorial(island.len())).product();
457
458    ScopeIterator {
459        expr_arena,
460        islands,
461        core,
462        current_index: 0,
463        total,
464        single_result: None,
465        returned_single: false,
466    }
467}
468
469fn group_by_island<'a>(quantifiers: Vec<QuantifierInfo<'a>>) -> Vec<Vec<QuantifierInfo<'a>>> {
470    use std::collections::BTreeMap;
471
472    let mut by_island: BTreeMap<u32, Vec<QuantifierInfo<'a>>> = BTreeMap::new();
473    for q in quantifiers {
474        by_island.entry(q.island_id).or_default().push(q);
475    }
476
477    by_island.into_values().collect()
478}
479
480fn group_scopal_by_island<'a>(elements: Vec<ScopalElement<'a>>) -> Vec<Vec<ScopalElement<'a>>> {
481    use std::collections::BTreeMap;
482
483    let mut by_island: BTreeMap<u32, Vec<ScopalElement<'a>>> = BTreeMap::new();
484    for elem in elements {
485        by_island.entry(elem.island_id()).or_default().push(elem);
486    }
487
488    by_island.into_values().collect()
489}
490
491fn extract_scopal_elements<'a>(
492    expr: &'a LogicExpr<'a>,
493    elements: &mut Vec<ScopalElement<'a>>,
494    interner: &mut Interner,
495    expr_arena: &'a Arena<LogicExpr<'a>>,
496) -> &'a LogicExpr<'a> {
497    match expr {
498        LogicExpr::Quantifier { kind, variable, body, island_id } => {
499            if let LogicExpr::BinaryOp { left, op, right } = body {
500                if matches!(op, TokenType::If | TokenType::And) {
501                    // Check if right side has a negation at the top level
502                    if let LogicExpr::UnaryOp { op: TokenType::Not, operand } = right {
503                        // Pattern: ∀x(R(x) → ¬P(x)) or ∃x(R(x) ∧ ¬P(x))
504                        // Extract both quantifier and negation
505                        elements.push(ScopalElement::Quantifier(QuantifierInfo {
506                            kind: *kind,
507                            variable: *variable,
508                            restrictor: *left,
509                            island_id: *island_id,
510                        }));
511                        elements.push(ScopalElement::Negation { island_id: *island_id });
512                        return extract_scopal_elements(operand, elements, interner, expr_arena);
513                    }
514                    // No negation in right side, just extract quantifier
515                    elements.push(ScopalElement::Quantifier(QuantifierInfo {
516                        kind: *kind,
517                        variable: *variable,
518                        restrictor: *left,
519                        island_id: *island_id,
520                    }));
521                    return extract_scopal_elements(right, elements, interner, expr_arena);
522                }
523            }
524            // No binary op body, use a true restrictor
525            elements.push(ScopalElement::Quantifier(QuantifierInfo {
526                kind: *kind,
527                variable: *variable,
528                restrictor: expr_arena.alloc(LogicExpr::Atom(interner.intern("T"))),
529                island_id: *island_id,
530            }));
531            extract_scopal_elements(body, elements, interner, expr_arena)
532        }
533        LogicExpr::UnaryOp { op: TokenType::Not, operand } => {
534            // Standalone negation (not inside a quantifier body)
535            elements.push(ScopalElement::Negation { island_id: 0 });
536            extract_scopal_elements(operand, elements, interner, expr_arena)
537        }
538        _ => expr,
539    }
540}
541
542fn rebuild_with_scopal_elements<'a>(
543    elements: &[ScopalElement<'a>],
544    core: &'a LogicExpr<'a>,
545    arena: &'a Arena<LogicExpr<'a>>,
546) -> &'a LogicExpr<'a> {
547    let mut result = core;
548
549    for elem in elements.iter().rev() {
550        match elem {
551            ScopalElement::Quantifier(q) => {
552                let connective = match q.kind {
553                    QuantifierKind::Universal => TokenType::If,
554                    _ => TokenType::And,
555                };
556
557                let body = arena.alloc(LogicExpr::BinaryOp {
558                    left: q.restrictor,
559                    op: connective,
560                    right: result,
561                });
562
563                result = arena.alloc(LogicExpr::Quantifier {
564                    kind: q.kind,
565                    variable: q.variable,
566                    body,
567                    island_id: q.island_id,
568                });
569            }
570            ScopalElement::Negation { .. } => {
571                result = arena.alloc(LogicExpr::UnaryOp {
572                    op: TokenType::Not,
573                    operand: result,
574                });
575            }
576        }
577    }
578
579    result
580}
581
582fn extract_quantifiers<'a>(
583    expr: &'a LogicExpr<'a>,
584    quantifiers: &mut Vec<QuantifierInfo<'a>>,
585    interner: &mut Interner,
586    expr_arena: &'a Arena<LogicExpr<'a>>,
587) -> &'a LogicExpr<'a> {
588    match expr {
589        LogicExpr::Quantifier { kind, variable, body, island_id } => {
590            if let LogicExpr::BinaryOp { left, op, right } = body {
591                if matches!(op, TokenType::If | TokenType::And) {
592                    quantifiers.push(QuantifierInfo {
593                        kind: *kind,
594                        variable: *variable,
595                        restrictor: *left,
596                        island_id: *island_id,
597                    });
598                    return extract_quantifiers(right, quantifiers, interner, expr_arena);
599                }
600            }
601            quantifiers.push(QuantifierInfo {
602                kind: *kind,
603                variable: *variable,
604                restrictor: expr_arena.alloc(LogicExpr::Atom(interner.intern("T"))),
605                island_id: *island_id,
606            });
607            extract_quantifiers(body, quantifiers, interner, expr_arena)
608        }
609        _ => expr,
610    }
611}
612
613fn rebuild_with_scope_order<'a>(
614    quantifiers: &[QuantifierInfo<'a>],
615    core: &'a LogicExpr<'a>,
616    arena: &'a Arena<LogicExpr<'a>>,
617) -> &'a LogicExpr<'a> {
618    let mut result = core;
619
620    for q in quantifiers.iter().rev() {
621        let connective = match q.kind {
622            QuantifierKind::Universal => TokenType::If,
623            _ => TokenType::And,
624        };
625
626        let body = arena.alloc(LogicExpr::BinaryOp {
627            left: q.restrictor,
628            op: connective,
629            right: result,
630        });
631
632        result = arena.alloc(LogicExpr::Quantifier {
633            kind: q.kind,
634            variable: q.variable,
635            body,
636            island_id: q.island_id,
637        });
638    }
639
640    result
641}
642
643pub fn lift_proper_name<'a>(
644    name: Symbol,
645    interner: &mut Interner,
646    arena: &'a Arena<LogicExpr<'a>>,
647) -> &'a LogicExpr<'a> {
648    let p_sym = interner.intern("P");
649    let inner_app = arena.alloc(LogicExpr::App {
650        function: arena.alloc(LogicExpr::Atom(p_sym)),
651        argument: arena.alloc(LogicExpr::Atom(name)),
652    });
653    arena.alloc(LogicExpr::Lambda {
654        variable: p_sym,
655        body: inner_app,
656    })
657}
658
659pub fn lift_quantifier<'a>(
660    kind: QuantifierKind,
661    restrictor: Symbol,
662    interner: &mut Interner,
663    expr_arena: &'a Arena<LogicExpr<'a>>,
664    term_arena: &'a Arena<Term<'a>>,
665) -> &'a LogicExpr<'a> {
666    let x_sym = interner.intern("x");
667    let q_sym = interner.intern("Q");
668
669    let restrictor_pred = expr_arena.alloc(LogicExpr::Predicate {
670        name: restrictor,
671        args: term_arena.alloc_slice([Term::Variable(x_sym)]),
672        world: None,
673    });
674
675    let q_of_x = expr_arena.alloc(LogicExpr::App {
676        function: expr_arena.alloc(LogicExpr::Atom(q_sym)),
677        argument: expr_arena.alloc(LogicExpr::Atom(x_sym)),
678    });
679
680    let connective = match kind {
681        QuantifierKind::Universal => TokenType::If,
682        _ => TokenType::And,
683    };
684
685    let body = expr_arena.alloc(LogicExpr::BinaryOp {
686        left: restrictor_pred,
687        op: connective,
688        right: q_of_x,
689    });
690
691    let quantifier = expr_arena.alloc(LogicExpr::Quantifier {
692        kind,
693        variable: x_sym,
694        body,
695        island_id: 0,
696    });
697
698    expr_arena.alloc(LogicExpr::Lambda {
699        variable: q_sym,
700        body: quantifier,
701    })
702}
703
704/// Performs beta reduction on lambda applications.
705///
706/// Reduces `(λx.body)(arg)` to `body[x := arg]` by substituting
707/// the argument for the bound variable in the body.
708pub fn beta_reduce<'a>(
709    expr: &'a LogicExpr<'a>,
710    expr_arena: &'a Arena<LogicExpr<'a>>,
711    term_arena: &'a Arena<Term<'a>>,
712) -> &'a LogicExpr<'a> {
713    match expr {
714        LogicExpr::App { function, argument } => {
715            if let LogicExpr::Lambda { variable, body } = function {
716                substitute(body, *variable, argument, expr_arena, term_arena)
717            } else {
718                expr_arena.alloc(LogicExpr::App {
719                    function: beta_reduce(function, expr_arena, term_arena),
720                    argument: beta_reduce(argument, expr_arena, term_arena),
721                })
722            }
723        }
724        LogicExpr::Lambda { variable, body } => expr_arena.alloc(LogicExpr::Lambda {
725            variable: *variable,
726            body: beta_reduce(body, expr_arena, term_arena),
727        }),
728        _ => expr,
729    }
730}
731
732fn substitute<'a>(
733    expr: &'a LogicExpr<'a>,
734    var: Symbol,
735    replacement: &'a LogicExpr<'a>,
736    expr_arena: &'a Arena<LogicExpr<'a>>,
737    term_arena: &'a Arena<Term<'a>>,
738) -> &'a LogicExpr<'a> {
739    match expr {
740        LogicExpr::Predicate { name, args, .. } => {
741            let new_args: Vec<Term<'a>> = args
742                .iter()
743                .map(|arg| substitute_term(arg, var, replacement, term_arena))
744                .collect();
745            expr_arena.alloc(LogicExpr::Predicate {
746                name: *name,
747                args: term_arena.alloc_slice(new_args),
748                world: None,
749            })
750        }
751
752        LogicExpr::Lambda { variable, body } => {
753            if *variable == var {
754                expr
755            } else {
756                expr_arena.alloc(LogicExpr::Lambda {
757                    variable: *variable,
758                    body: substitute(body, var, replacement, expr_arena, term_arena),
759                })
760            }
761        }
762
763        LogicExpr::App { function, argument } => expr_arena.alloc(LogicExpr::App {
764            function: substitute(function, var, replacement, expr_arena, term_arena),
765            argument: substitute(argument, var, replacement, expr_arena, term_arena),
766        }),
767
768        LogicExpr::BinaryOp { left, op, right } => expr_arena.alloc(LogicExpr::BinaryOp {
769            left: substitute(left, var, replacement, expr_arena, term_arena),
770            op: op.clone(),
771            right: substitute(right, var, replacement, expr_arena, term_arena),
772        }),
773
774        LogicExpr::UnaryOp { op, operand } => expr_arena.alloc(LogicExpr::UnaryOp {
775            op: op.clone(),
776            operand: substitute(operand, var, replacement, expr_arena, term_arena),
777        }),
778
779        LogicExpr::Quantifier { kind, variable, body, island_id } => {
780            if *variable == var {
781                expr
782            } else {
783                expr_arena.alloc(LogicExpr::Quantifier {
784                    kind: *kind,
785                    variable: *variable,
786                    body: substitute(body, var, replacement, expr_arena, term_arena),
787                    island_id: *island_id,
788                })
789            }
790        }
791
792        LogicExpr::Atom(s) => {
793            if *s == var {
794                replacement
795            } else {
796                expr
797            }
798        }
799
800        _ => expr,
801    }
802}
803
804fn substitute_term<'a>(
805    term: &Term<'a>,
806    var: Symbol,
807    replacement: &LogicExpr<'a>,
808    term_arena: &'a Arena<Term<'a>>,
809) -> Term<'a> {
810    match term {
811        Term::Variable(v) if *v == var => {
812            match replacement {
813                LogicExpr::Atom(s) => Term::Constant(*s),
814                LogicExpr::Predicate { name, .. } => Term::Constant(*name),
815                _ => clone_term(term, term_arena),
816            }
817        }
818        _ => clone_term(term, term_arena),
819    }
820}
821
822// ═══════════════════════════════════════════════════════════════════
823// Intensional Reading Generation (De Re / De Dicto)
824// ═══════════════════════════════════════════════════════════════════
825
826#[derive(Debug)]
827struct IntensionalContext {
828    verb: Symbol,
829    quantifier_var: Symbol,
830    restrictor: Symbol,
831}
832
833fn find_opaque_verb_context<'a>(
834    expr: &'a LogicExpr<'a>,
835    interner: &Interner,
836) -> Option<IntensionalContext> {
837    match expr {
838        LogicExpr::Quantifier { kind: QuantifierKind::Existential, variable, body, .. } => {
839            if let LogicExpr::BinaryOp { left, op: TokenType::And, right } = body {
840                if let LogicExpr::Predicate { name: restrictor, args, .. } = left {
841                    if args.len() == 1 {
842                        if let Term::Variable(v) = &args[0] {
843                            if *v == *variable {
844                                if let Some(verb) = find_opaque_verb_in_scope(right, *variable, interner) {
845                                    return Some(IntensionalContext {
846                                        verb,
847                                        quantifier_var: *variable,
848                                        restrictor: *restrictor,
849                                    });
850                                }
851                            }
852                        }
853                    }
854                }
855            }
856            None
857        }
858        _ => None,
859    }
860}
861
862fn find_opaque_verb_in_scope<'a>(
863    expr: &'a LogicExpr<'a>,
864    theme_var: Symbol,
865    interner: &Interner,
866) -> Option<Symbol> {
867    match expr {
868        LogicExpr::Quantifier { body, .. } => find_opaque_verb_in_scope(body, theme_var, interner),
869        LogicExpr::BinaryOp { left, right, .. } => {
870            find_opaque_verb_in_scope(left, theme_var, interner)
871                .or_else(|| find_opaque_verb_in_scope(right, theme_var, interner))
872        }
873        LogicExpr::NeoEvent(data) => {
874            if is_opaque_verb(data.verb, interner) {
875                for (role, term) in data.roles.iter() {
876                    if matches!(role, crate::ast::ThematicRole::Theme) {
877                        if let Term::Variable(v) = term {
878                            if *v == theme_var {
879                                return Some(data.verb);
880                            }
881                        }
882                    }
883                }
884            }
885            None
886        }
887        LogicExpr::Predicate { name, args, .. } => {
888            if is_opaque_verb(*name, interner) && args.len() >= 2 {
889                if let Term::Variable(v) = &args[1] {
890                    if *v == theme_var {
891                        return Some(*name);
892                    }
893                }
894            }
895            None
896        }
897        _ => None,
898    }
899}
900
901fn build_de_dicto_reading<'a>(
902    expr: &'a LogicExpr<'a>,
903    ctx: &IntensionalContext,
904    expr_arena: &'a Arena<LogicExpr<'a>>,
905    term_arena: &'a Arena<Term<'a>>,
906    role_arena: &'a Arena<(crate::ast::ThematicRole, Term<'a>)>,
907) -> &'a LogicExpr<'a> {
908    match expr {
909        LogicExpr::Quantifier { kind: QuantifierKind::Existential, variable, body, .. }
910            if *variable == ctx.quantifier_var =>
911        {
912            if let LogicExpr::BinaryOp { right, .. } = body {
913                replace_theme_with_intension(right, ctx, expr_arena, term_arena, role_arena)
914            } else {
915                expr
916            }
917        }
918        _ => expr,
919    }
920}
921
922fn replace_theme_with_intension<'a>(
923    expr: &'a LogicExpr<'a>,
924    ctx: &IntensionalContext,
925    expr_arena: &'a Arena<LogicExpr<'a>>,
926    term_arena: &'a Arena<Term<'a>>,
927    role_arena: &'a Arena<(crate::ast::ThematicRole, Term<'a>)>,
928) -> &'a LogicExpr<'a> {
929    match expr {
930        LogicExpr::Quantifier { kind, variable, body, island_id } => {
931            let new_body = replace_theme_with_intension(body, ctx, expr_arena, term_arena, role_arena);
932            expr_arena.alloc(LogicExpr::Quantifier {
933                kind: *kind,
934                variable: *variable,
935                body: new_body,
936                island_id: *island_id,
937            })
938        }
939        LogicExpr::BinaryOp { left, op, right } => {
940            let new_left = replace_theme_with_intension(left, ctx, expr_arena, term_arena, role_arena);
941            let new_right = replace_theme_with_intension(right, ctx, expr_arena, term_arena, role_arena);
942            expr_arena.alloc(LogicExpr::BinaryOp {
943                left: new_left,
944                op: op.clone(),
945                right: new_right,
946            })
947        }
948        LogicExpr::NeoEvent(data) => {
949            let new_roles: Vec<_> = data.roles.iter().map(|(role, term)| {
950                if matches!(role, crate::ast::ThematicRole::Theme) {
951                    if let Term::Variable(v) = term {
952                        if *v == ctx.quantifier_var {
953                            return (*role, Term::Intension(ctx.restrictor));
954                        }
955                    }
956                }
957                (*role, clone_term(term, term_arena))
958            }).collect();
959
960            expr_arena.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
961                event_var: data.event_var,
962                verb: data.verb,
963                roles: role_arena.alloc_slice(new_roles),
964                modifiers: data.modifiers,
965                suppress_existential: false,
966                world: None,
967            })))
968        }
969        LogicExpr::Predicate { name, args, .. } => {
970            let new_args: Vec<_> = args.iter().map(|arg| {
971                if let Term::Variable(v) = arg {
972                    if *v == ctx.quantifier_var {
973                        return Term::Intension(ctx.restrictor);
974                    }
975                }
976                clone_term(arg, term_arena)
977            }).collect();
978
979            expr_arena.alloc(LogicExpr::Predicate {
980                name: *name,
981                args: term_arena.alloc_slice(new_args),
982                world: None,
983            })
984        }
985        _ => expr,
986    }
987}
988
989pub fn enumerate_intensional_readings<'a>(
990    expr: &'a LogicExpr<'a>,
991    interner: &mut Interner,
992    expr_arena: &'a Arena<LogicExpr<'a>>,
993    term_arena: &'a Arena<Term<'a>>,
994    role_arena: &'a Arena<(crate::ast::ThematicRole, Term<'a>)>,
995) -> Vec<&'a LogicExpr<'a>> {
996    // Check if expression already has intensional terms (de dicto from parser)
997    if let Some(de_re) = build_de_re_from_de_dicto(expr, interner, expr_arena, term_arena, role_arena) {
998        // Return both: de re first (existential), de dicto second (intension)
999        return vec![de_re, expr];
1000    }
1001
1002    // Original logic: check for de re that can be converted to de dicto
1003    if let Some(ctx) = find_opaque_verb_context(expr, interner) {
1004        let de_dicto = build_de_dicto_reading(expr, &ctx, expr_arena, term_arena, role_arena);
1005        vec![expr, de_dicto]
1006    } else {
1007        vec![expr]
1008    }
1009}
1010
1011fn build_de_re_from_de_dicto<'a>(
1012    expr: &'a LogicExpr<'a>,
1013    interner: &mut Interner,
1014    expr_arena: &'a Arena<LogicExpr<'a>>,
1015    term_arena: &'a Arena<Term<'a>>,
1016    role_arena: &'a Arena<(crate::ast::ThematicRole, Term<'a>)>,
1017) -> Option<&'a LogicExpr<'a>> {
1018    // Find Term::Intension in NeoEvent themes and expand to existential
1019    match expr {
1020        LogicExpr::NeoEvent(data) => {
1021            // Check if any role has an Intension term
1022            for (role, term) in data.roles.iter() {
1023                if matches!(role, crate::ast::ThematicRole::Theme) {
1024                    if let Term::Intension(noun) = term {
1025                        // Build de re: ∃x(Noun(x) ∧ Event[Theme=x])
1026                        let var = interner.intern("x");
1027
1028                        // Build noun predicate: Noun(x)
1029                        let noun_pred = expr_arena.alloc(LogicExpr::Predicate {
1030                            name: *noun,
1031                            args: term_arena.alloc_slice([Term::Variable(var)]),
1032                            world: None,
1033                        });
1034
1035                        // Build new roles with variable instead of intension
1036                        let new_roles: Vec<_> = data.roles.iter().map(|(r, t)| {
1037                            if matches!(r, crate::ast::ThematicRole::Theme) {
1038                                (*r, Term::Variable(var))
1039                            } else {
1040                                (*r, t.clone())
1041                            }
1042                        }).collect();
1043
1044                        let new_event = expr_arena.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
1045                            event_var: data.event_var,
1046                            verb: data.verb,
1047                            roles: role_arena.alloc_slice(new_roles),
1048                            modifiers: data.modifiers,
1049                            suppress_existential: false,
1050                            world: None,
1051                        })));
1052
1053                        // Build: ∃x(Noun(x) ∧ Event)
1054                        let body = expr_arena.alloc(LogicExpr::BinaryOp {
1055                            left: noun_pred,
1056                            op: crate::token::TokenType::And,
1057                            right: new_event,
1058                        });
1059
1060                        return Some(expr_arena.alloc(LogicExpr::Quantifier {
1061                            kind: crate::ast::QuantifierKind::Existential,
1062                            variable: var,
1063                            body,
1064                            island_id: 0,
1065                        }));
1066                    }
1067                }
1068            }
1069            None
1070        }
1071        _ => None,
1072    }
1073}
1074
1075#[cfg(test)]
1076mod tests {
1077    use super::*;
1078    use crate::ast::{LogicExpr, Term};
1079    use logicaffeine_base::Interner;
1080    use crate::registry::SymbolRegistry;
1081    use crate::OutputFormat;
1082
1083    #[test]
1084    fn test_lambda_formatting_unicode() {
1085        let mut interner = Interner::new();
1086        let expr_arena: Arena<LogicExpr> = Arena::new();
1087        let term_arena: Arena<Term> = Arena::new();
1088
1089        let x = interner.intern("x");
1090        let sleep = interner.intern("Sleep");
1091
1092        let body = expr_arena.alloc(LogicExpr::Predicate {
1093            name: sleep,
1094            args: term_arena.alloc_slice([Term::Variable(x)]),
1095            world: None,
1096        });
1097        let lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body });
1098
1099        let mut registry = SymbolRegistry::new();
1100        let output = lambda.transpile(&mut registry, &interner, OutputFormat::Unicode);
1101        assert!(output.contains("λx"), "Unicode should use λ: {}", output);
1102    }
1103
1104    #[test]
1105    fn test_lambda_formatting_latex() {
1106        let mut interner = Interner::new();
1107        let expr_arena: Arena<LogicExpr> = Arena::new();
1108        let term_arena: Arena<Term> = Arena::new();
1109
1110        let x = interner.intern("x");
1111        let sleep = interner.intern("Sleep");
1112
1113        let body = expr_arena.alloc(LogicExpr::Predicate {
1114            name: sleep,
1115            args: term_arena.alloc_slice([Term::Variable(x)]),
1116            world: None,
1117        });
1118        let lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body });
1119
1120        let mut registry = SymbolRegistry::new();
1121        let output = lambda.transpile(&mut registry, &interner, OutputFormat::LaTeX);
1122        assert!(output.contains("\\lambda"), "LaTeX should use \\lambda: {}", output);
1123    }
1124
1125    #[test]
1126    fn test_application_formatting() {
1127        let mut interner = Interner::new();
1128        let expr_arena: Arena<LogicExpr> = Arena::new();
1129
1130        let p = interner.intern("P");
1131        let j = interner.intern("j");
1132
1133        let func = expr_arena.alloc(LogicExpr::Atom(p));
1134        let arg = expr_arena.alloc(LogicExpr::Atom(j));
1135        let app = expr_arena.alloc(LogicExpr::App { function: func, argument: arg });
1136
1137        let mut registry = SymbolRegistry::new();
1138        let output = app.transpile(&mut registry, &interner, OutputFormat::Unicode);
1139        assert!(output.contains("(") && output.contains(")"), "App should have parens: {}", output);
1140    }
1141
1142    #[test]
1143    fn test_nested_lambda() {
1144        let mut interner = Interner::new();
1145        let expr_arena: Arena<LogicExpr> = Arena::new();
1146
1147        let x = interner.intern("x");
1148        let y = interner.intern("y");
1149
1150        let inner_body = expr_arena.alloc(LogicExpr::Atom(x));
1151        let inner_lambda = expr_arena.alloc(LogicExpr::Lambda { variable: y, body: inner_body });
1152        let outer_lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body: inner_lambda });
1153
1154        let mut registry = SymbolRegistry::new();
1155        let output = outer_lambda.transpile(&mut registry, &interner, OutputFormat::Unicode);
1156        assert!(output.contains("λx") && output.contains("λy"), "Nested lambdas: {}", output);
1157    }
1158
1159    #[test]
1160    fn test_lambda_app_helper_functions() {
1161        let mut interner = Interner::new();
1162        let expr_arena: Arena<LogicExpr> = Arena::new();
1163        let _term_arena: Arena<Term> = Arena::new();
1164
1165        let x = interner.intern("x");
1166        let p = interner.intern("P");
1167
1168        let body = expr_arena.alloc(LogicExpr::Atom(x));
1169        let lambda = LogicExpr::lambda(x, body, &expr_arena);
1170
1171        let arg = expr_arena.alloc(LogicExpr::Atom(p));
1172        let app = LogicExpr::app(lambda, arg, &expr_arena);
1173
1174        assert!(matches!(app, LogicExpr::App { .. }));
1175    }
1176
1177    #[test]
1178    fn lift_proper_name_returns_lambda() {
1179        let mut interner = Interner::new();
1180        let arena: Arena<LogicExpr> = Arena::new();
1181
1182        let john = interner.intern("John");
1183        let lifted = lift_proper_name(john, &mut interner, &arena);
1184
1185        assert!(matches!(lifted, LogicExpr::Lambda { .. }), "Should return Lambda");
1186    }
1187
1188    #[test]
1189    fn lift_proper_name_applies_predicate() {
1190        let mut interner = Interner::new();
1191        let arena: Arena<LogicExpr> = Arena::new();
1192
1193        let john = interner.intern("John");
1194        let lifted = lift_proper_name(john, &mut interner, &arena);
1195
1196        if let LogicExpr::Lambda { body, .. } = lifted {
1197            assert!(matches!(body, LogicExpr::App { .. }), "Body should be App");
1198        } else {
1199            panic!("Expected Lambda");
1200        }
1201    }
1202
1203    #[test]
1204    fn lift_quantifier_universal_returns_lambda() {
1205        let mut interner = Interner::new();
1206        let expr_arena: Arena<LogicExpr> = Arena::new();
1207        let term_arena: Arena<Term> = Arena::new();
1208
1209        let woman = interner.intern("woman");
1210        let lifted = lift_quantifier(QuantifierKind::Universal, woman, &mut interner, &expr_arena, &term_arena);
1211
1212        assert!(matches!(lifted, LogicExpr::Lambda { .. }), "Should return Lambda");
1213    }
1214
1215    #[test]
1216    fn lift_quantifier_universal_structure() {
1217        let mut interner = Interner::new();
1218        let expr_arena: Arena<LogicExpr> = Arena::new();
1219        let term_arena: Arena<Term> = Arena::new();
1220
1221        let woman = interner.intern("woman");
1222        let lifted = lift_quantifier(QuantifierKind::Universal, woman, &mut interner, &expr_arena, &term_arena);
1223
1224        if let LogicExpr::Lambda { body, .. } = lifted {
1225            assert!(
1226                matches!(body, LogicExpr::Quantifier { kind: QuantifierKind::Universal, .. }),
1227                "Body should contain ∀, got {:?}",
1228                body
1229            );
1230        } else {
1231            panic!("Expected Lambda, got {:?}", lifted);
1232        }
1233    }
1234
1235    #[test]
1236    fn lift_quantifier_existential_returns_lambda() {
1237        let mut interner = Interner::new();
1238        let expr_arena: Arena<LogicExpr> = Arena::new();
1239        let term_arena: Arena<Term> = Arena::new();
1240
1241        let man = interner.intern("man");
1242        let lifted = lift_quantifier(QuantifierKind::Existential, man, &mut interner, &expr_arena, &term_arena);
1243
1244        assert!(matches!(lifted, LogicExpr::Lambda { .. }), "Should return Lambda");
1245    }
1246
1247    #[test]
1248    fn lift_quantifier_existential_structure() {
1249        let mut interner = Interner::new();
1250        let expr_arena: Arena<LogicExpr> = Arena::new();
1251        let term_arena: Arena<Term> = Arena::new();
1252
1253        let man = interner.intern("man");
1254        let lifted = lift_quantifier(QuantifierKind::Existential, man, &mut interner, &expr_arena, &term_arena);
1255
1256        if let LogicExpr::Lambda { body, .. } = lifted {
1257            assert!(
1258                matches!(body, LogicExpr::Quantifier { kind: QuantifierKind::Existential, .. }),
1259                "Body should contain ∃, got {:?}",
1260                body
1261            );
1262        } else {
1263            panic!("Expected Lambda, got {:?}", lifted);
1264        }
1265    }
1266
1267    #[test]
1268    fn beta_reduce_simple_predicate() {
1269        let mut interner = Interner::new();
1270        let expr_arena: Arena<LogicExpr> = Arena::new();
1271        let term_arena: Arena<Term> = Arena::new();
1272
1273        let x = interner.intern("x");
1274        let john = interner.intern("John");
1275        let run = interner.intern("Run");
1276
1277        let body = expr_arena.alloc(LogicExpr::Predicate {
1278            name: run,
1279            args: term_arena.alloc_slice([Term::Variable(x)]),
1280            world: None,
1281        });
1282        let lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body });
1283        let arg = expr_arena.alloc(LogicExpr::Atom(john));
1284        let app = expr_arena.alloc(LogicExpr::App { function: lambda, argument: arg });
1285
1286        let reduced = beta_reduce(app, &expr_arena, &term_arena);
1287
1288        let mut registry = SymbolRegistry::new();
1289        let output = reduced.transpile(&mut registry, &interner, OutputFormat::Unicode);
1290        assert!(output.contains("R(J)") || output.contains("Run(John)"), "Should substitute: {}", output);
1291    }
1292
1293    #[test]
1294    fn beta_reduce_with_constant() {
1295        let mut interner = Interner::new();
1296        let expr_arena: Arena<LogicExpr> = Arena::new();
1297        let term_arena: Arena<Term> = Arena::new();
1298
1299        let x = interner.intern("x");
1300        let c = interner.intern("c");
1301
1302        let body = expr_arena.alloc(LogicExpr::Atom(c));
1303        let lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body });
1304        let arg = expr_arena.alloc(LogicExpr::Atom(interner.intern("anything")));
1305        let app = expr_arena.alloc(LogicExpr::App { function: lambda, argument: arg });
1306
1307        let reduced = beta_reduce(app, &expr_arena, &term_arena);
1308        assert!(matches!(reduced, LogicExpr::Atom(s) if *s == c), "Constant should remain");
1309    }
1310
1311    #[test]
1312    fn beta_reduce_nested_lambda() {
1313        let mut interner = Interner::new();
1314        let expr_arena: Arena<LogicExpr> = Arena::new();
1315        let term_arena: Arena<Term> = Arena::new();
1316
1317        let x = interner.intern("x");
1318        let y = interner.intern("y");
1319
1320        let inner_body = expr_arena.alloc(LogicExpr::Atom(x));
1321        let inner_lambda = expr_arena.alloc(LogicExpr::Lambda { variable: y, body: inner_body });
1322        let outer_lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body: inner_lambda });
1323
1324        let reduced = beta_reduce(outer_lambda, &expr_arena, &term_arena);
1325        assert!(matches!(reduced, LogicExpr::Lambda { .. }), "Should still be lambda");
1326    }
1327
1328    #[test]
1329    fn beta_reduce_non_application_unchanged() {
1330        let mut interner = Interner::new();
1331        let expr_arena: Arena<LogicExpr> = Arena::new();
1332        let term_arena: Arena<Term> = Arena::new();
1333
1334        let p = interner.intern("P");
1335        let atom = expr_arena.alloc(LogicExpr::Atom(p));
1336
1337        let reduced = beta_reduce(atom, &expr_arena, &term_arena);
1338        assert!(matches!(reduced, LogicExpr::Atom(s) if *s == p), "Atom unchanged");
1339    }
1340
1341    #[test]
1342    fn beta_reduce_preserves_unbound_variables() {
1343        let mut interner = Interner::new();
1344        let expr_arena: Arena<LogicExpr> = Arena::new();
1345        let term_arena: Arena<Term> = Arena::new();
1346
1347        let x = interner.intern("x");
1348        let y = interner.intern("y");
1349        let john = interner.intern("John");
1350        let loves = interner.intern("Loves");
1351
1352        let body = expr_arena.alloc(LogicExpr::Predicate {
1353            name: loves,
1354            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y)]),
1355            world: None,
1356        });
1357        let lambda = expr_arena.alloc(LogicExpr::Lambda { variable: x, body });
1358        let arg = expr_arena.alloc(LogicExpr::Atom(john));
1359        let app = expr_arena.alloc(LogicExpr::App { function: lambda, argument: arg });
1360
1361        let reduced = beta_reduce(app, &expr_arena, &term_arena);
1362
1363        let mut registry = SymbolRegistry::new();
1364        let output = reduced.transpile(&mut registry, &interner, OutputFormat::Unicode);
1365        assert!(output.contains("y"), "y should remain unbound: {}", output);
1366    }
1367
1368    #[test]
1369    fn enumerate_scopings_single_quantifier() {
1370        let mut interner = Interner::new();
1371        let expr_arena: Arena<LogicExpr> = Arena::new();
1372        let term_arena: Arena<Term> = Arena::new();
1373
1374        let x = interner.intern("x");
1375        let dog = interner.intern("Dog");
1376        let bark = interner.intern("Bark");
1377
1378        let left = expr_arena.alloc(LogicExpr::Predicate {
1379            name: dog,
1380            args: term_arena.alloc_slice([Term::Variable(x)]),
1381            world: None,
1382        });
1383        let right = expr_arena.alloc(LogicExpr::Predicate {
1384            name: bark,
1385            args: term_arena.alloc_slice([Term::Variable(x)]),
1386            world: None,
1387        });
1388        let body = expr_arena.alloc(LogicExpr::BinaryOp {
1389            left,
1390            op: TokenType::If,
1391            right,
1392        });
1393        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1394            kind: QuantifierKind::Universal,
1395            variable: x,
1396            body,
1397            island_id: 0,
1398        });
1399
1400        let scopings = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena);
1401        assert_eq!(scopings.len(), 1, "Single quantifier should have 1 reading");
1402    }
1403
1404    #[test]
1405    fn enumerate_scopings_no_quantifier() {
1406        let mut interner = Interner::new();
1407        let expr_arena: Arena<LogicExpr> = Arena::new();
1408        let term_arena: Arena<Term> = Arena::new();
1409
1410        let run = interner.intern("Run");
1411        let john = interner.intern("John");
1412
1413        let expr = expr_arena.alloc(LogicExpr::Predicate {
1414            name: run,
1415            args: term_arena.alloc_slice([Term::Constant(john)]),
1416            world: None,
1417        });
1418
1419        let scopings = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena);
1420        assert_eq!(scopings.len(), 1, "No quantifiers should have 1 reading");
1421    }
1422
1423    #[test]
1424    fn is_opaque_verb_believes() {
1425        let mut interner = Interner::new();
1426        let believes = interner.intern("believes");
1427        let believes_cap = interner.intern("Believes");
1428        assert!(is_opaque_verb(believes, &interner), "believes should be opaque");
1429        assert!(is_opaque_verb(believes_cap, &interner), "Believes should be opaque");
1430    }
1431
1432    #[test]
1433    fn is_opaque_verb_seeks() {
1434        let mut interner = Interner::new();
1435        let seeks = interner.intern("seeks");
1436        let wants = interner.intern("wants");
1437        assert!(is_opaque_verb(seeks, &interner), "seeks should be opaque");
1438        assert!(is_opaque_verb(wants, &interner), "wants should be opaque");
1439    }
1440
1441    #[test]
1442    fn is_opaque_verb_normal_verbs() {
1443        let mut interner = Interner::new();
1444        let runs = interner.intern("runs");
1445        let loves = interner.intern("loves");
1446        assert!(!is_opaque_verb(runs, &interner), "runs should NOT be opaque");
1447        assert!(!is_opaque_verb(loves, &interner), "loves should NOT be opaque");
1448    }
1449
1450    #[test]
1451    fn make_intensional_creates_wrapper() {
1452        let mut interner = Interner::new();
1453        let expr_arena: Arena<LogicExpr> = Arena::new();
1454        let term_arena: Arena<Term> = Arena::new();
1455
1456        let weak = interner.intern("Weak");
1457        let clark = interner.intern("Clark");
1458        let believes = interner.intern("believes");
1459
1460        let content = expr_arena.alloc(LogicExpr::Predicate {
1461            name: weak,
1462            args: term_arena.alloc_slice([Term::Constant(clark)]),
1463            world: None,
1464        });
1465
1466        let intensional = make_intensional(believes, content, &expr_arena);
1467
1468        assert!(
1469            matches!(intensional, LogicExpr::Intensional { operator, .. } if *operator == believes),
1470            "Should create Intensional wrapper, got {:?}",
1471            intensional
1472        );
1473    }
1474
1475    #[test]
1476    fn intensional_transpiles_with_brackets() {
1477        let mut interner = Interner::new();
1478        let expr_arena: Arena<LogicExpr> = Arena::new();
1479        let term_arena: Arena<Term> = Arena::new();
1480
1481        let weak = interner.intern("Weak");
1482        let clark = interner.intern("Clark");
1483        let believes = interner.intern("Believes");
1484
1485        let content = expr_arena.alloc(LogicExpr::Predicate {
1486            name: weak,
1487            args: term_arena.alloc_slice([Term::Constant(clark)]),
1488            world: None,
1489        });
1490
1491        let intensional = expr_arena.alloc(LogicExpr::Intensional {
1492            operator: believes,
1493            content,
1494        });
1495
1496        let mut registry = SymbolRegistry::new();
1497        let output = intensional.transpile(&mut registry, &interner, OutputFormat::Unicode);
1498
1499        assert!(
1500            output.contains("[") && output.contains("]"),
1501            "Intensional should use brackets: got {}",
1502            output
1503        );
1504    }
1505
1506    #[test]
1507    fn substitute_respecting_opacity_blocks_inside_intensional() {
1508        let mut interner = Interner::new();
1509        let expr_arena: Arena<LogicExpr> = Arena::new();
1510        let term_arena: Arena<Term> = Arena::new();
1511
1512        let weak = interner.intern("Weak");
1513        let clark = interner.intern("Clark");
1514        let believes = interner.intern("Believes");
1515        let superman = interner.intern("Superman");
1516
1517        let inner = expr_arena.alloc(LogicExpr::Predicate {
1518            name: weak,
1519            args: term_arena.alloc_slice([Term::Constant(clark)]),
1520            world: None,
1521        });
1522        let expr = expr_arena.alloc(LogicExpr::Intensional {
1523            operator: believes,
1524            content: inner,
1525        });
1526
1527        let replacement = expr_arena.alloc(LogicExpr::Atom(superman));
1528        let result = substitute_respecting_opacity(expr, clark, replacement, &expr_arena, &term_arena);
1529
1530        let mut registry = SymbolRegistry::new();
1531        let output = result.transpile(&mut registry, &interner, OutputFormat::Unicode);
1532
1533        assert!(
1534            output.contains("C") && !output.contains("S"),
1535            "Should NOT substitute inside intensional context: got {}",
1536            output
1537        );
1538    }
1539
1540    #[test]
1541    fn substitute_respecting_opacity_allows_outside() {
1542        let mut interner = Interner::new();
1543        let expr_arena: Arena<LogicExpr> = Arena::new();
1544        let term_arena: Arena<Term> = Arena::new();
1545
1546        let weak = interner.intern("Weak");
1547        let clark = interner.intern("Clark");
1548        let superman = interner.intern("Superman");
1549
1550        let expr = expr_arena.alloc(LogicExpr::Predicate {
1551            name: weak,
1552            args: term_arena.alloc_slice([Term::Constant(clark)]),
1553            world: None,
1554        });
1555
1556        let replacement = expr_arena.alloc(LogicExpr::Atom(superman));
1557        let result = substitute_respecting_opacity(expr, clark, replacement, &expr_arena, &term_arena);
1558
1559        let mut registry = SymbolRegistry::new();
1560        let output = result.transpile(&mut registry, &interner, OutputFormat::Unicode);
1561
1562        assert!(
1563            output.contains("S"),
1564            "Should substitute outside intensional context: got {}",
1565            output
1566        );
1567    }
1568
1569    #[test]
1570    fn factorial_basic() {
1571        assert_eq!(factorial(0), 1);
1572        assert_eq!(factorial(1), 1);
1573        assert_eq!(factorial(2), 2);
1574        assert_eq!(factorial(3), 6);
1575        assert_eq!(factorial(4), 24);
1576        assert_eq!(factorial(5), 120);
1577    }
1578
1579    #[test]
1580    fn scope_iterator_two_quantifiers_yields_two() {
1581        let mut interner = Interner::new();
1582        let expr_arena: Arena<LogicExpr> = Arena::new();
1583        let term_arena: Arena<Term> = Arena::new();
1584
1585        let x = interner.intern("x");
1586        let y = interner.intern("y");
1587        let man = interner.intern("Man");
1588        let woman = interner.intern("Woman");
1589        let loves = interner.intern("Loves");
1590
1591        let man_x = expr_arena.alloc(LogicExpr::Predicate {
1592            name: man,
1593            args: term_arena.alloc_slice([Term::Variable(x)]),
1594            world: None,
1595        });
1596        let woman_y = expr_arena.alloc(LogicExpr::Predicate {
1597            name: woman,
1598            args: term_arena.alloc_slice([Term::Variable(y)]),
1599            world: None,
1600        });
1601        let loves_xy = expr_arena.alloc(LogicExpr::Predicate {
1602            name: loves,
1603            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y)]),
1604            world: None,
1605        });
1606
1607        let inner = expr_arena.alloc(LogicExpr::BinaryOp {
1608            left: woman_y,
1609            op: TokenType::And,
1610            right: loves_xy,
1611        });
1612        let inner_q = expr_arena.alloc(LogicExpr::Quantifier {
1613            kind: QuantifierKind::Existential,
1614            variable: y,
1615            body: inner,
1616            island_id: 0,
1617        });
1618
1619        let outer = expr_arena.alloc(LogicExpr::BinaryOp {
1620            left: man_x,
1621            op: TokenType::If,
1622            right: inner_q,
1623        });
1624        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1625            kind: QuantifierKind::Universal,
1626            variable: x,
1627            body: outer,
1628            island_id: 0,
1629        });
1630
1631        let scopings: Vec<_> = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena).collect();
1632        assert_eq!(scopings.len(), 2, "Two quantifiers should have 2! = 2 readings");
1633    }
1634
1635    #[test]
1636    fn scope_iterator_three_quantifiers_yields_six() {
1637        let mut interner = Interner::new();
1638        let expr_arena: Arena<LogicExpr> = Arena::new();
1639        let term_arena: Arena<Term> = Arena::new();
1640
1641        let x = interner.intern("x");
1642        let y = interner.intern("y");
1643        let z = interner.intern("z");
1644        let man = interner.intern("Man");
1645        let woman = interner.intern("Woman");
1646        let book = interner.intern("Book");
1647        let gives = interner.intern("Gives");
1648
1649        let man_x = expr_arena.alloc(LogicExpr::Predicate {
1650            name: man,
1651            args: term_arena.alloc_slice([Term::Variable(x)]),
1652            world: None,
1653        });
1654        let woman_y = expr_arena.alloc(LogicExpr::Predicate {
1655            name: woman,
1656            args: term_arena.alloc_slice([Term::Variable(y)]),
1657            world: None,
1658        });
1659        let book_z = expr_arena.alloc(LogicExpr::Predicate {
1660            name: book,
1661            args: term_arena.alloc_slice([Term::Variable(z)]),
1662            world: None,
1663        });
1664        let gives_xyz = expr_arena.alloc(LogicExpr::Predicate {
1665            name: gives,
1666            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y), Term::Variable(z)]),
1667            world: None,
1668        });
1669
1670        let inner_z = expr_arena.alloc(LogicExpr::BinaryOp {
1671            left: book_z,
1672            op: TokenType::And,
1673            right: gives_xyz,
1674        });
1675        let q_z = expr_arena.alloc(LogicExpr::Quantifier {
1676            kind: QuantifierKind::Existential,
1677            variable: z,
1678            body: inner_z,
1679            island_id: 0,
1680        });
1681
1682        let inner_y = expr_arena.alloc(LogicExpr::BinaryOp {
1683            left: woman_y,
1684            op: TokenType::And,
1685            right: q_z,
1686        });
1687        let q_y = expr_arena.alloc(LogicExpr::Quantifier {
1688            kind: QuantifierKind::Existential,
1689            variable: y,
1690            body: inner_y,
1691            island_id: 0,
1692        });
1693
1694        let outer = expr_arena.alloc(LogicExpr::BinaryOp {
1695            left: man_x,
1696            op: TokenType::If,
1697            right: q_y,
1698        });
1699        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1700            kind: QuantifierKind::Universal,
1701            variable: x,
1702            body: outer,
1703            island_id: 0,
1704        });
1705
1706        let scopings: Vec<_> = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena).collect();
1707        assert_eq!(scopings.len(), 6, "Three quantifiers should have 3! = 6 readings");
1708    }
1709
1710    #[test]
1711    fn scope_iterator_no_duplicates() {
1712        use std::collections::HashSet;
1713
1714        let mut interner = Interner::new();
1715        let expr_arena: Arena<LogicExpr> = Arena::new();
1716        let term_arena: Arena<Term> = Arena::new();
1717
1718        let x = interner.intern("x");
1719        let y = interner.intern("y");
1720        let man = interner.intern("Man");
1721        let woman = interner.intern("Woman");
1722        let loves = interner.intern("Loves");
1723
1724        let man_x = expr_arena.alloc(LogicExpr::Predicate {
1725            name: man,
1726            args: term_arena.alloc_slice([Term::Variable(x)]),
1727            world: None,
1728        });
1729        let woman_y = expr_arena.alloc(LogicExpr::Predicate {
1730            name: woman,
1731            args: term_arena.alloc_slice([Term::Variable(y)]),
1732            world: None,
1733        });
1734        let loves_xy = expr_arena.alloc(LogicExpr::Predicate {
1735            name: loves,
1736            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y)]),
1737            world: None,
1738        });
1739
1740        let inner = expr_arena.alloc(LogicExpr::BinaryOp {
1741            left: woman_y,
1742            op: TokenType::And,
1743            right: loves_xy,
1744        });
1745        let inner_q = expr_arena.alloc(LogicExpr::Quantifier {
1746            kind: QuantifierKind::Existential,
1747            variable: y,
1748            body: inner,
1749            island_id: 0,
1750        });
1751
1752        let outer = expr_arena.alloc(LogicExpr::BinaryOp {
1753            left: man_x,
1754            op: TokenType::If,
1755            right: inner_q,
1756        });
1757        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1758            kind: QuantifierKind::Universal,
1759            variable: x,
1760            body: outer,
1761            island_id: 0,
1762        });
1763
1764        let mut registry = SymbolRegistry::new();
1765        let outputs: HashSet<String> = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena)
1766            .map(|e| e.transpile(&mut registry, &interner, OutputFormat::Unicode))
1767            .collect();
1768
1769        assert_eq!(outputs.len(), 2, "All scopings should be unique");
1770    }
1771
1772    #[test]
1773    fn scope_iterator_exact_size() {
1774        let mut interner = Interner::new();
1775        let expr_arena: Arena<LogicExpr> = Arena::new();
1776        let term_arena: Arena<Term> = Arena::new();
1777
1778        let x = interner.intern("x");
1779        let y = interner.intern("y");
1780        let man = interner.intern("Man");
1781        let woman = interner.intern("Woman");
1782        let loves = interner.intern("Loves");
1783
1784        let man_x = expr_arena.alloc(LogicExpr::Predicate {
1785            name: man,
1786            args: term_arena.alloc_slice([Term::Variable(x)]),
1787            world: None,
1788        });
1789        let woman_y = expr_arena.alloc(LogicExpr::Predicate {
1790            name: woman,
1791            args: term_arena.alloc_slice([Term::Variable(y)]),
1792            world: None,
1793        });
1794        let loves_xy = expr_arena.alloc(LogicExpr::Predicate {
1795            name: loves,
1796            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y)]),
1797            world: None,
1798        });
1799
1800        let inner = expr_arena.alloc(LogicExpr::BinaryOp {
1801            left: woman_y,
1802            op: TokenType::And,
1803            right: loves_xy,
1804        });
1805        let inner_q = expr_arena.alloc(LogicExpr::Quantifier {
1806            kind: QuantifierKind::Existential,
1807            variable: y,
1808            body: inner,
1809            island_id: 0,
1810        });
1811
1812        let outer = expr_arena.alloc(LogicExpr::BinaryOp {
1813            left: man_x,
1814            op: TokenType::If,
1815            right: inner_q,
1816        });
1817        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1818            kind: QuantifierKind::Universal,
1819            variable: x,
1820            body: outer,
1821            island_id: 0,
1822        });
1823
1824        let mut iter = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena);
1825        assert_eq!(iter.len(), 2);
1826        iter.next();
1827        assert_eq!(iter.len(), 1);
1828        iter.next();
1829        assert_eq!(iter.len(), 0);
1830    }
1831
1832    #[test]
1833    fn island_constraints_reduce_permutations() {
1834        let mut interner = Interner::new();
1835        let expr_arena: Arena<LogicExpr> = Arena::new();
1836        let term_arena: Arena<Term> = Arena::new();
1837
1838        let x = interner.intern("x");
1839        let y = interner.intern("y");
1840        let man = interner.intern("Man");
1841        let woman = interner.intern("Woman");
1842        let loves = interner.intern("Loves");
1843
1844        let man_x = expr_arena.alloc(LogicExpr::Predicate {
1845            name: man,
1846            args: term_arena.alloc_slice([Term::Variable(x)]),
1847            world: None,
1848        });
1849        let woman_y = expr_arena.alloc(LogicExpr::Predicate {
1850            name: woman,
1851            args: term_arena.alloc_slice([Term::Variable(y)]),
1852            world: None,
1853        });
1854        let loves_xy = expr_arena.alloc(LogicExpr::Predicate {
1855            name: loves,
1856            args: term_arena.alloc_slice([Term::Variable(x), Term::Variable(y)]),
1857            world: None,
1858        });
1859
1860        let inner = expr_arena.alloc(LogicExpr::BinaryOp {
1861            left: woman_y,
1862            op: TokenType::And,
1863            right: loves_xy,
1864        });
1865        let inner_q = expr_arena.alloc(LogicExpr::Quantifier {
1866            kind: QuantifierKind::Existential,
1867            variable: y,
1868            body: inner,
1869            island_id: 1,
1870        });
1871
1872        let outer = expr_arena.alloc(LogicExpr::BinaryOp {
1873            left: man_x,
1874            op: TokenType::If,
1875            right: inner_q,
1876        });
1877        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1878            kind: QuantifierKind::Universal,
1879            variable: x,
1880            body: outer,
1881            island_id: 0,
1882        });
1883
1884        let scopings = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena);
1885        assert_eq!(
1886            scopings.len(),
1887            1,
1888            "Two quantifiers in different islands: 1! × 1! = 1 reading (no cross-island scoping)"
1889        );
1890    }
1891
1892    #[test]
1893    fn multiple_quantifiers_per_island() {
1894        let mut interner = Interner::new();
1895        let expr_arena: Arena<LogicExpr> = Arena::new();
1896        let term_arena: Arena<Term> = Arena::new();
1897
1898        let x = interner.intern("x");
1899        let y = interner.intern("y");
1900        let z = interner.intern("z");
1901        let w = interner.intern("w");
1902        let pred = interner.intern("P");
1903
1904        let core = expr_arena.alloc(LogicExpr::Predicate {
1905            name: pred,
1906            args: term_arena.alloc_slice([
1907                Term::Variable(x),
1908                Term::Variable(y),
1909                Term::Variable(z),
1910                Term::Variable(w),
1911            ]),
1912            world: None,
1913        });
1914
1915        let true_sym = interner.intern("T");
1916        let t = expr_arena.alloc(LogicExpr::Atom(true_sym));
1917
1918        let q_w = expr_arena.alloc(LogicExpr::Quantifier {
1919            kind: QuantifierKind::Existential,
1920            variable: w,
1921            body: expr_arena.alloc(LogicExpr::BinaryOp { left: t, op: TokenType::And, right: core }),
1922            island_id: 1,
1923        });
1924        let q_z = expr_arena.alloc(LogicExpr::Quantifier {
1925            kind: QuantifierKind::Existential,
1926            variable: z,
1927            body: expr_arena.alloc(LogicExpr::BinaryOp { left: t, op: TokenType::And, right: q_w }),
1928            island_id: 1,
1929        });
1930        let q_y = expr_arena.alloc(LogicExpr::Quantifier {
1931            kind: QuantifierKind::Existential,
1932            variable: y,
1933            body: expr_arena.alloc(LogicExpr::BinaryOp { left: t, op: TokenType::And, right: q_z }),
1934            island_id: 0,
1935        });
1936        let expr = expr_arena.alloc(LogicExpr::Quantifier {
1937            kind: QuantifierKind::Universal,
1938            variable: x,
1939            body: expr_arena.alloc(LogicExpr::BinaryOp { left: t, op: TokenType::If, right: q_y }),
1940            island_id: 0,
1941        });
1942
1943        let scopings = enumerate_scopings(expr, &mut interner, &expr_arena, &term_arena);
1944        assert_eq!(
1945            scopings.len(),
1946            4,
1947            "4 quantifiers split 2+2 across islands: 2! × 2! = 4 (not 4! = 24)"
1948        );
1949    }
1950}
logicaffeine_language/lambda.rs

logicaffeine_language/
lambda.rs
