oxilean_std/lambda_calculus/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::UsageMap;
6use super::functions::*;
7
8/// Strategy for β-reduction.
9#[derive(Debug, Clone, Copy, PartialEq, Eq)]
10pub enum Strategy {
11    /// Normal order (leftmost-outermost).
12    NormalOrder,
13    /// Applicative order (leftmost-innermost / call-by-value).
14    ApplicativeOrder,
15    /// Head reduction (reduce only the head redex).
16    HeadReduction,
17}
18/// Check α-equivalence of two terms (de Bruijn terms are equal up to renaming
19/// of bound variables by definition — so alpha-equivalence is just structural equality
20/// after normalization of bound variable names, which in de Bruijn form is plain equality).
21#[allow(dead_code)]
22pub struct AlphaEquivalenceChecker;
23#[allow(dead_code)]
24impl AlphaEquivalenceChecker {
25    /// Create a new checker.
26    pub fn new() -> Self {
27        AlphaEquivalenceChecker
28    }
29    /// Check whether two terms are alpha-equivalent.
30    /// With de Bruijn indices, alpha-equivalence is structural equality.
31    pub fn alpha_equiv(&self, t1: &Term, t2: &Term) -> bool {
32        t1 == t2
33    }
34    /// Check alpha-equivalence modulo one layer of beta-reduction.
35    /// Useful when terms may differ by a single administrative redex.
36    pub fn alpha_equiv_after_head_step(&self, t1: &Term, t2: &Term) -> bool {
37        if self.alpha_equiv(t1, t2) {
38            return true;
39        }
40        let s1 = beta_step(t1, Strategy::HeadReduction).unwrap_or_else(|| t1.clone());
41        let s2 = beta_step(t2, Strategy::HeadReduction).unwrap_or_else(|| t2.clone());
42        self.alpha_equiv(&s1, &s2)
43    }
44    /// Check whether two terms are alpha-equivalent after full normalization
45    /// (with a step limit).
46    pub fn alpha_equiv_normalized(&self, t1: &Term, t2: &Term, limit: usize) -> bool {
47        let (n1, _) = t1.normalize(limit);
48        let (n2, _) = t2.normalize(limit);
49        self.alpha_equiv(&n1, &n2)
50    }
51}
52/// A β-reducer with configurable strategy and step budget.
53#[allow(dead_code)]
54pub struct BetaReducer {
55    strategy: Strategy,
56    max_steps: usize,
57}
58#[allow(dead_code)]
59impl BetaReducer {
60    /// Create a new reducer with the given strategy and step limit.
61    pub fn new(strategy: Strategy, max_steps: usize) -> Self {
62        BetaReducer {
63            strategy,
64            max_steps,
65        }
66    }
67    /// Reduce the term to normal form under the configured strategy.
68    /// Returns `(result, steps_taken, converged)`.
69    pub fn reduce(&self, term: &Term) -> (Term, usize, bool) {
70        let mut current = term.clone();
71        let mut steps = 0;
72        loop {
73            if steps >= self.max_steps {
74                return (current, steps, false);
75            }
76            match beta_step(&current, self.strategy) {
77                None => return (current, steps, true),
78                Some(next) => {
79                    current = next;
80                    steps += 1;
81                }
82            }
83        }
84    }
85    /// Check if a term is already in normal form under this strategy.
86    pub fn is_normal_form(&self, term: &Term) -> bool {
87        beta_step(term, self.strategy).is_none()
88    }
89    /// Count reduction steps without storing intermediate terms.
90    pub fn count_steps(&self, term: &Term) -> Option<usize> {
91        let (_, steps, converged) = self.reduce(term);
92        if converged {
93            Some(steps)
94        } else {
95            None
96        }
97    }
98}
99/// A simple type: base or arrow.
100#[derive(Debug, Clone, PartialEq, Eq)]
101pub enum SimpleType {
102    /// A base type with a name (e.g., "o", "ι").
103    Base(String),
104    /// Function type A → B.
105    Arrow(Box<SimpleType>, Box<SimpleType>),
106}
107impl SimpleType {
108    /// Arrow type constructor (convenience).
109    pub fn arr(a: SimpleType, b: SimpleType) -> Self {
110        SimpleType::Arrow(Box::new(a), Box::new(b))
111    }
112}
113/// A typing context: list of types for de Bruijn variables.
114/// Index 0 = innermost binder.
115#[derive(Debug, Clone)]
116pub struct Context(pub Vec<SimpleType>);
117impl Context {
118    /// Empty context.
119    pub fn empty() -> Self {
120        Context(vec![])
121    }
122    /// Extend the context with a new type (push to front = index 0).
123    pub fn extend(&self, ty: SimpleType) -> Context {
124        let mut v = vec![ty];
125        v.extend(self.0.clone());
126        Context(v)
127    }
128    /// Look up the type of de Bruijn variable `k`.
129    pub fn get(&self, k: usize) -> Option<&SimpleType> {
130        self.0.get(k)
131    }
132}
133/// Checks compatibility (duality) between two session types.
134#[allow(dead_code)]
135pub struct SessionTypeCompatibility;
136#[allow(dead_code)]
137impl SessionTypeCompatibility {
138    /// Create a new compatibility checker.
139    pub fn new() -> Self {
140        SessionTypeCompatibility
141    }
142    /// Compute the dual of a session type (swap sends↔receives, select↔offer).
143    pub fn dual(&self, s: &BinarySession) -> BinarySession {
144        match s {
145            BinarySession::Send(label, cont) => {
146                BinarySession::Recv(label.clone(), Box::new(self.dual(cont)))
147            }
148            BinarySession::Recv(label, cont) => {
149                BinarySession::Send(label.clone(), Box::new(self.dual(cont)))
150            }
151            BinarySession::Select(branches) => {
152                let dual_branches: Vec<(String, BinarySession)> = branches
153                    .iter()
154                    .map(|(l, s)| (l.clone(), self.dual(s)))
155                    .collect();
156                BinarySession::Offer(dual_branches)
157            }
158            BinarySession::Offer(branches) => {
159                let dual_branches: Vec<(String, BinarySession)> = branches
160                    .iter()
161                    .map(|(l, s)| (l.clone(), self.dual(s)))
162                    .collect();
163                BinarySession::Select(dual_branches)
164            }
165            BinarySession::Rec(x, body) => BinarySession::Rec(x.clone(), Box::new(self.dual(body))),
166            BinarySession::Var(x) => BinarySession::Var(x.clone()),
167            BinarySession::End => BinarySession::End,
168        }
169    }
170    /// Check whether `s1` and `s2` are dual (i.e., compatible).
171    /// A process holding `s1` can communicate with one holding `s2`.
172    pub fn are_dual(&self, s1: &BinarySession, s2: &BinarySession) -> bool {
173        &self.dual(s1) == s2
174    }
175    /// Check that a pair of sessions can reduce to `End` together (session progress).
176    /// This is a simple syntactic check: both are End, or both are dual in one step.
177    pub fn compatible(&self, s1: &BinarySession, s2: &BinarySession) -> bool {
178        match (s1, s2) {
179            (BinarySession::End, BinarySession::End) => true,
180            (BinarySession::Send(l1, c1), BinarySession::Recv(l2, c2)) => {
181                l1 == l2 && self.compatible(c1, c2)
182            }
183            (BinarySession::Recv(l1, c1), BinarySession::Send(l2, c2)) => {
184                l1 == l2 && self.compatible(c1, c2)
185            }
186            (BinarySession::Select(bs1), BinarySession::Offer(bs2)) => bs1.iter().all(|(l, s)| {
187                bs2.iter()
188                    .find(|(l2, _)| l == l2)
189                    .map(|(_, s2)| self.compatible(s, s2))
190                    .unwrap_or(false)
191            }),
192            (BinarySession::Offer(bs1), BinarySession::Select(bs2)) => bs2.iter().all(|(l, s)| {
193                bs1.iter()
194                    .find(|(l1, _)| l == l1)
195                    .map(|(_, s1)| self.compatible(s1, s))
196                    .unwrap_or(false)
197            }),
198            _ => false,
199        }
200    }
201}
202/// An untyped lambda calculus term using de Bruijn indices.
203#[derive(Debug, Clone, PartialEq, Eq)]
204pub enum Term {
205    /// de Bruijn variable (0 = innermost binder).
206    Var(usize),
207    /// Lambda abstraction: λ.body.
208    Lam(Box<Term>),
209    /// Application: (f arg).
210    App(Box<Term>, Box<Term>),
211}
212impl Term {
213    /// Shift all free variables by `d` when entering a context of depth `cutoff`.
214    pub fn shift(&self, d: isize, cutoff: usize) -> Term {
215        match self {
216            Term::Var(k) => {
217                if *k >= cutoff {
218                    let new_k = (*k as isize + d) as usize;
219                    Term::Var(new_k)
220                } else {
221                    Term::Var(*k)
222                }
223            }
224            Term::Lam(body) => Term::Lam(Box::new(body.shift(d, cutoff + 1))),
225            Term::App(f, a) => {
226                Term::App(Box::new(f.shift(d, cutoff)), Box::new(a.shift(d, cutoff)))
227            }
228        }
229    }
230    /// Substitute `sub` for de Bruijn index `j` in `self`.
231    pub fn subst(&self, j: usize, sub: &Term) -> Term {
232        match self {
233            Term::Var(k) => {
234                if *k == j {
235                    sub.shift(j as isize, 0)
236                } else if *k > j {
237                    Term::Var(k - 1)
238                } else {
239                    Term::Var(*k)
240                }
241            }
242            Term::Lam(body) => Term::Lam(Box::new(body.subst(j + 1, sub))),
243            Term::App(f, a) => Term::App(Box::new(f.subst(j, sub)), Box::new(a.subst(j, sub))),
244        }
245    }
246    /// Perform one step of β-reduction (normal order: leftmost-outermost).
247    /// Returns `Some(reduced)` if a redex was found, `None` if already normal.
248    pub fn beta_step_normal(&self) -> Option<Term> {
249        match self {
250            Term::App(f, a) => {
251                if let Term::Lam(body) = f.as_ref() {
252                    return Some(body.subst(0, a));
253                }
254                if let Some(f2) = f.beta_step_normal() {
255                    return Some(Term::App(Box::new(f2), a.clone()));
256                }
257                if let Some(a2) = a.beta_step_normal() {
258                    return Some(Term::App(f.clone(), Box::new(a2)));
259                }
260                None
261            }
262            Term::Lam(body) => body.beta_step_normal().map(|b2| Term::Lam(Box::new(b2))),
263            Term::Var(_) => None,
264        }
265    }
266    /// Fully normalize by normal-order β-reduction (with a step limit to avoid divergence).
267    pub fn normalize(&self, limit: usize) -> (Term, usize) {
268        let mut t = self.clone();
269        let mut steps = 0;
270        while steps < limit {
271            match t.beta_step_normal() {
272                Some(t2) => {
273                    t = t2;
274                    steps += 1;
275                }
276                None => break,
277            }
278        }
279        (t, steps)
280    }
281    /// Check if the term is in beta-normal form.
282    pub fn is_normal(&self) -> bool {
283        self.beta_step_normal().is_none()
284    }
285    /// Count the number of nodes in the term tree.
286    pub fn size(&self) -> usize {
287        match self {
288            Term::Var(_) => 1,
289            Term::Lam(b) => 1 + b.size(),
290            Term::App(f, a) => 1 + f.size() + a.size(),
291        }
292    }
293}
294/// A bidirectional type inference system for STLC.
295/// Implements the "Check" and "Synth" modes of bidirectional typing.
296#[allow(dead_code)]
297pub struct TypeInferenceSystem;
298#[allow(dead_code)]
299impl TypeInferenceSystem {
300    /// Create a new type inference system.
301    pub fn new() -> Self {
302        TypeInferenceSystem
303    }
304    /// Synthesis mode: try to infer the type of `term` in context `ctx`.
305    /// Returns `Some(ty)` if successful.
306    pub fn synthesize(&self, ctx: &Context, term: &Term) -> Option<SimpleType> {
307        match term {
308            Term::Var(k) => ctx.get(*k).cloned(),
309            Term::App(f, a) => {
310                let ft = self.synthesize(ctx, f)?;
311                match ft {
312                    SimpleType::Arrow(dom, cod) => {
313                        if self.check(ctx, a, &dom) {
314                            Some(*cod)
315                        } else {
316                            None
317                        }
318                    }
319                    _ => None,
320                }
321            }
322            Term::Lam(_) => None,
323        }
324    }
325    /// Checking mode: verify that `term` has type `ty` in context `ctx`.
326    pub fn check(&self, ctx: &Context, term: &Term, ty: &SimpleType) -> bool {
327        match (term, ty) {
328            (Term::Lam(body), SimpleType::Arrow(dom, cod)) => {
329                let extended = ctx.extend(*dom.clone());
330                self.check(&extended, body, cod)
331            }
332            _ => match self.synthesize(ctx, term) {
333                Some(inferred) => inferred == *ty,
334                None => false,
335            },
336        }
337    }
338    /// Attempt to reconstruct the type of an annotated term.
339    /// A term is "annotated" if it is an application with a synthesizable function.
340    pub fn infer_with_annotation(
341        &self,
342        ctx: &Context,
343        term: &Term,
344        hint: Option<&SimpleType>,
345    ) -> Option<SimpleType> {
346        match hint {
347            Some(ty) => {
348                if self.check(ctx, term, ty) {
349                    Some(ty.clone())
350                } else {
351                    None
352                }
353            }
354            None => self.synthesize(ctx, term),
355        }
356    }
357}
358/// A simple linearity checker that tracks variable usage counts.
359/// In linear typing, each variable must be used exactly once.
360#[allow(dead_code)]
361pub struct LinearTypeChecker;
362#[allow(dead_code)]
363impl LinearTypeChecker {
364    /// Create a new linearity checker.
365    pub fn new() -> Self {
366        LinearTypeChecker
367    }
368    /// Count free variable occurrences in `term`, relative to a context of `depth` variables.
369    /// Returns a vector of length `depth` with usage counts for each variable.
370    pub fn count_uses(&self, term: &Term, depth: usize) -> UsageMap {
371        let mut counts = vec![0usize; depth];
372        self.count_uses_inner(term, depth, 0, &mut counts);
373        counts
374    }
375    fn count_uses_inner(&self, term: &Term, depth: usize, offset: usize, counts: &mut UsageMap) {
376        match term {
377            Term::Var(k) => {
378                let adjusted = if *k >= offset { k - offset } else { return };
379                if adjusted < depth {
380                    counts[adjusted] += 1;
381                }
382            }
383            Term::Lam(body) => {
384                self.count_uses_inner(body, depth, offset + 1, counts);
385            }
386            Term::App(f, a) => {
387                self.count_uses_inner(f, depth, offset, counts);
388                self.count_uses_inner(a, depth, offset, counts);
389            }
390        }
391    }
392    /// Check if `term` is linear in the context of `depth` variables.
393    /// Returns `true` iff every variable in the context is used exactly once.
394    pub fn is_linear(&self, term: &Term, depth: usize) -> bool {
395        let uses = self.count_uses(term, depth);
396        uses.iter().all(|&c| c == 1)
397    }
398    /// Check if `term` is affine in the context of `depth` variables.
399    /// Returns `true` iff every variable in the context is used at most once.
400    pub fn is_affine(&self, term: &Term, depth: usize) -> bool {
401        let uses = self.count_uses(term, depth);
402        uses.iter().all(|&c| c <= 1)
403    }
404    /// Check if `term` is relevant in the context of `depth` variables.
405    /// Returns `true` iff every variable in the context is used at least once.
406    pub fn is_relevant(&self, term: &Term, depth: usize) -> bool {
407        let uses = self.count_uses(term, depth);
408        uses.iter().all(|&c| c >= 1)
409    }
410}
411/// A session type in the binary session type system.
412#[derive(Debug, Clone, PartialEq, Eq)]
413pub enum BinarySession {
414    /// Send a value of type `label` and continue as `next`.
415    Send(String, Box<BinarySession>),
416    /// Receive a value of type `label` and continue as `next`.
417    Recv(String, Box<BinarySession>),
418    /// Internal choice: select one of the offered branches.
419    Select(Vec<(String, BinarySession)>),
420    /// External choice: offer a set of branches.
421    Offer(Vec<(String, BinarySession)>),
422    /// Recursive session: μX.S where `name` is the recursion variable.
423    Rec(String, Box<BinarySession>),
424    /// Session variable reference.
425    Var(String),
426    /// Completed session.
427    End,
428}
oxilean_std/lambda_calculus/types.rs

oxilean_std/lambda_calculus/
types.rs
