Enum LogicExpr 

pub enum LogicExpr<'a> {
    Predicate {
        name: Symbol,
        args: &'a [Term<'a>],
        world: Option<Symbol>,
    },
    Identity {
        left: &'a Term<'a>,
        right: &'a Term<'a>,
    },
    Metaphor {
        tenor: &'a Term<'a>,
        vehicle: &'a Term<'a>,
    },
    Quantifier {
        kind: QuantifierKind,
        variable: Symbol,
        body: &'a LogicExpr<'a>,
        island_id: u32,
    },
    Categorical(Box<CategoricalData<'a>>),
    Relation(Box<RelationData<'a>>),
    Modal {
        vector: ModalVector,
        operand: &'a LogicExpr<'a>,
    },
    Temporal {
        operator: TemporalOperator,
        body: &'a LogicExpr<'a>,
    },
    TemporalBinary {
        operator: BinaryTemporalOp,
        left: &'a LogicExpr<'a>,
        right: &'a LogicExpr<'a>,
    },
    Aspectual {
        operator: AspectOperator,
        body: &'a LogicExpr<'a>,
    },
    Voice {
        operator: VoiceOperator,
        body: &'a LogicExpr<'a>,
    },
    BinaryOp {
        left: &'a LogicExpr<'a>,
        op: TokenType,
        right: &'a LogicExpr<'a>,
    },
    UnaryOp {
        op: TokenType,
        operand: &'a LogicExpr<'a>,
    },
    Question {
        wh_variable: Symbol,
        body: &'a LogicExpr<'a>,
    },
    YesNoQuestion {
        body: &'a LogicExpr<'a>,
    },
    Atom(Symbol),
    Lambda {
        variable: Symbol,
        body: &'a LogicExpr<'a>,
    },
    App {
        function: &'a LogicExpr<'a>,
        argument: &'a LogicExpr<'a>,
    },
    Intensional {
        operator: Symbol,
        content: &'a LogicExpr<'a>,
    },
    Event {
        predicate: &'a LogicExpr<'a>,
        adverbs: &'a [Symbol],
    },
    NeoEvent(Box<NeoEventData<'a>>),
    Imperative {
        action: &'a LogicExpr<'a>,
    },
    Exclamative {
        degree_var: Symbol,
        body: &'a LogicExpr<'a>,
    },
    Optative {
        wish: &'a LogicExpr<'a>,
    },
    Implicature {
        assertion: &'a LogicExpr<'a>,
        implicature: &'a LogicExpr<'a>,
    },
    SpeechAct {
        performer: Symbol,
        act_type: Symbol,
        content: &'a LogicExpr<'a>,
    },
    Counterfactual {
        antecedent: &'a LogicExpr<'a>,
        consequent: &'a LogicExpr<'a>,
    },
    Causal {
        effect: &'a LogicExpr<'a>,
        cause: &'a LogicExpr<'a>,
    },
    Concessive {
        main: &'a LogicExpr<'a>,
        concession: &'a LogicExpr<'a>,
    },
    Comparative {
        adjective: Symbol,
        subject: &'a Term<'a>,
        object: &'a Term<'a>,
        difference: Option<&'a Term<'a>>,
        relation: ComparisonRelation,
    },
    Superlative {
        adjective: Symbol,
        subject: &'a Term<'a>,
        domain: Symbol,
    },
    Scopal {
        operator: Symbol,
        body: &'a LogicExpr<'a>,
    },
    Control {
        verb: Symbol,
        subject: &'a Term<'a>,
        object: Option<&'a Term<'a>>,
        infinitive: &'a LogicExpr<'a>,
    },
    Presupposition {
        assertion: &'a LogicExpr<'a>,
        presupposition: &'a LogicExpr<'a>,
    },
    Focus {
        kind: FocusKind,
        focused: &'a Term<'a>,
        scope: &'a LogicExpr<'a>,
    },
    TemporalAnchor {
        anchor: Symbol,
        body: &'a LogicExpr<'a>,
    },
    Distributive {
        predicate: &'a LogicExpr<'a>,
    },
    GroupQuantifier {
        group_var: Symbol,
        count: u32,
        member_var: Symbol,
        restriction: &'a LogicExpr<'a>,
        body: &'a LogicExpr<'a>,
    },
}

First-order logic expression with modal, temporal, and event extensions.

This is the core AST type representing logical formulas. All nodes are arena-allocated with the 'a lifetime tracking the arena’s scope.

Categories

• Core FOL: Predicate, Quantifier, BinaryOp, UnaryOp, Identity
• Lambda calculus: Lambda, App, Atom
• Modal logic: Modal, Intensional
• Temporal/Aspect: Temporal, Aspectual, Voice
• Event semantics: Event, NeoEvent
• Questions: Question, YesNoQuestion
• Pragmatics: SpeechAct, Focus, Presupposition
• Comparison: Comparative, Superlative
• Other: Counterfactual, Causal, Control, Imperative

Variants

Predicate

Atomic predicate: P(t1, t2, ...) with optional world parameter.

Fields

name: Symbol

args: &'a [Term<'a>]

world: Option<Symbol>

World argument for Kripke semantics. None = implicit actual world (w₀).

Identity

Identity statement: t1 = t2.

Fields

left: &'a Term<'a>

right: &'a Term<'a>

Metaphor

Metaphorical assertion: tenor “is” vehicle (non-literal identity).

Fields

tenor: &'a Term<'a>

vehicle: &'a Term<'a>

Quantifier

Quantified formula: ∀x.φ or ∃x.φ with scope island tracking.

Fields

kind: QuantifierKind

variable: Symbol

body: &'a LogicExpr<'a>

island_id: u32

Island ID prevents illicit scope interactions across syntactic boundaries.

Categorical(Box<CategoricalData<'a>>)

Aristotelian categorical proposition (boxed to keep enum small).

Relation(Box<RelationData<'a>>)

Simple S-V-O relation (boxed).

Modal

Modal operator: □φ (necessity) or ◇φ (possibility).

Fields

vector: ModalVector

operand: &'a LogicExpr<'a>

Temporal

Tense/temporal operator: PAST(φ), FUTURE(φ), ALWAYS(φ), EVENTUALLY(φ), NEXT(φ).

Fields

operator: TemporalOperator

body: &'a LogicExpr<'a>

TemporalBinary

Binary temporal operator: φ UNTIL ψ, φ RELEASE ψ, φ WEAKUNTIL ψ.

Fields

operator: BinaryTemporalOp

left: &'a LogicExpr<'a>

right: &'a LogicExpr<'a>

Aspectual

Aspect operator: PROG(φ), PERF(φ), HAB(φ), ITER(φ).

Fields

operator: AspectOperator

body: &'a LogicExpr<'a>

Voice

Voice operator: PASSIVE(φ).

Fields

operator: VoiceOperator

body: &'a LogicExpr<'a>

BinaryOp

Binary connective: φ ∧ ψ, φ ∨ ψ, φ → ψ, φ ↔ ψ.

Fields

left: &'a LogicExpr<'a>

op: TokenType

right: &'a LogicExpr<'a>

UnaryOp

Unary operator: ¬φ.

Fields

op: TokenType

operand: &'a LogicExpr<'a>

Question

Wh-question: λx.φ where x is the questioned variable.

Fields

wh_variable: Symbol

body: &'a LogicExpr<'a>

YesNoQuestion

Yes/no question: ?φ (is φ true?).

Fields

body: &'a LogicExpr<'a>

Atom(Symbol)

Atomic symbol (variable or constant in lambda context).

Lambda

Lambda abstraction: λx.φ.

Fields

variable: Symbol

body: &'a LogicExpr<'a>

App

Function application: (φ)(ψ).

Fields

function: &'a LogicExpr<'a>

argument: &'a LogicExpr<'a>

Intensional

Intensional context: operator[content] for opaque verbs (believes, seeks).

Fields

operator: Symbol

content: &'a LogicExpr<'a>

Event

Legacy event semantics (Davidson-style with adverb list).

Fields

predicate: &'a LogicExpr<'a>

adverbs: &'a [Symbol]

NeoEvent(Box<NeoEventData<'a>>)

Neo-Davidsonian event with thematic roles (boxed).

Imperative

Imperative command: !φ.

Fields

action: &'a LogicExpr<'a>

Exclamative

Exclamative: affective stance toward a surprisingly-high degree, with no subject-aux inversion (“How tall she is!”, “What a fool he is!”). Asserts ∃degree_var(body ∧ degree_var ≫ θ) and presupposes body.

Fields

degree_var: Symbol

body: &'a LogicExpr<'a>

Optative

Optative: a wish with no asserted truth (“May you prosper!”, “Long live the king!”, “If only it were Friday!”). → Wish(speaker, ⟨wish⟩); the complement is NOT entailed.

Fields

wish: &'a LogicExpr<'a>

Implicature

Scalar implicature (§8.7): a weak scalar item asserts assertion and DEFEASIBLY implicates implicature (the negation of a stronger Horn alternative). “Some students passed.” → ∃… +> ¬∀…. Rendered assertion +> implicature; the implicature is cancellable and not part of truth conditions.

Fields

assertion: &'a LogicExpr<'a>

implicature: &'a LogicExpr<'a>

SpeechAct

Speech act: performative utterance with illocutionary force.

Fields

performer: Symbol

act_type: Symbol

content: &'a LogicExpr<'a>

Counterfactual

Counterfactual conditional: “If P had been, Q would have been”.

Fields

antecedent: &'a LogicExpr<'a>

consequent: &'a LogicExpr<'a>

Causal

Causal relation: “effect because cause”.

Fields

effect: &'a LogicExpr<'a>

cause: &'a LogicExpr<'a>

Concessive

Concessive relation: “main, although concession” — the main clause holds DESPITE a defeated expectation from the concession (“Although she was tired, she finished.” → Finish(she) ∧ Concessive(Tired(she))).

Fields

main: &'a LogicExpr<'a>

concession: &'a LogicExpr<'a>

Comparative

Comparative / equative: “X is taller than Y” (>), “X is as tall as Y” (≥), “X is as tall as Y and no taller” (=). The relation selects the degree comparison; difference is the optional measure (“by 2 inches”).

Fields

adjective: Symbol

subject: &'a Term<'a>

object: &'a Term<'a>

difference: Option<&'a Term<'a>>

relation: ComparisonRelation

Superlative

Superlative: “X is the tallest among domain”.

Fields

adjective: Symbol

subject: &'a Term<'a>

domain: Symbol

Scopal

Scopal adverb: “only”, “always”, etc. as operators.

Fields

operator: Symbol

body: &'a LogicExpr<'a>

Control

Control verb: “wants to VP”, “persuaded X to VP”.

Fields

verb: Symbol

subject: &'a Term<'a>

object: Option<&'a Term<'a>>

infinitive: &'a LogicExpr<'a>

Presupposition

Presupposition-assertion structure.

Fields

assertion: &'a LogicExpr<'a>

presupposition: &'a LogicExpr<'a>

Focus

Focus particle: “only X”, “even X” with alternative set.

Fields

kind: FocusKind

focused: &'a Term<'a>

scope: &'a LogicExpr<'a>

TemporalAnchor

Temporal anchor: “yesterday(φ)”, “now(φ)”.

Fields

anchor: Symbol

body: &'a LogicExpr<'a>

Distributive

Distributive operator: *P distributes P over group members.

Fields

predicate: &'a LogicExpr<'a>

GroupQuantifier

Group quantifier for collective cardinal readings. ∃g(Group(g) ∧ Count(g,n) ∧ ∀x(Member(x,g) → Restriction(x)) ∧ Body(g))

Fields

group_var: Symbol

count: u32

member_var: Symbol

restriction: &'a LogicExpr<'a>

body: &'a LogicExpr<'a>

Implementations

impl<'a> LogicExpr<'a>

pub fn lambda( var: Symbol, body: &'a LogicExpr<'a>, arena: &'a Arena<LogicExpr<'a>>, ) -> &'a LogicExpr<'a>

pub fn app( func: &'a LogicExpr<'a>, arg: &'a LogicExpr<'a>, arena: &'a Arena<LogicExpr<'a>>, ) -> &'a LogicExpr<'a>

impl<'a> LogicExpr<'a>

pub fn transpile_discourse( &self, registry: &mut SymbolRegistry, interner: &Interner, format: OutputFormat, ) -> String

Transpile a discourse (multiple sentences) as numbered formulas. If the expression is a top-level conjunction of sentences, formats as:

1) formula1
2) formula2
3) formula3

If it’s a single sentence, just returns the formula without numbering.

pub fn write_logic<W, F>( &self, w: &mut W, registry: &mut SymbolRegistry, interner: &Interner, fmt: &F, ) -> Result<(), Error>

where W: Write, F: LogicFormatter,

pub fn transpile_with<F>( &self, registry: &mut SymbolRegistry, interner: &Interner, fmt: &F, ) -> String

where F: LogicFormatter,

Transpiles to a logic formula string using a custom formatter.

pub fn transpile( &self, registry: &mut SymbolRegistry, interner: &Interner, format: OutputFormat, ) -> String

Transpiles to a logic formula string in the specified output format.

Formats

• OutputFormat::Unicode: ∀x(Cat(x) → Sleeps(x))
• OutputFormat::LaTeX: \forall x(Cat(x) \to Sleeps(x))
• OutputFormat::SimpleFOL: Ax(Cat(x) -> Sleeps(x))
• OutputFormat::Kripke: □(P) @w0

pub fn transpile_ctx<F>( &self, ctx: &mut TranspileContext<'_>, fmt: &F, ) -> String

where F: LogicFormatter,

Transpiles using a TranspileContext and custom formatter.

pub fn transpile_ctx_unicode(&self, ctx: &mut TranspileContext<'_>) -> String

Transpiles to Unicode format using a TranspileContext.

pub fn transpile_ctx_latex(&self, ctx: &mut TranspileContext<'_>) -> String

Transpiles to LaTeX format using a TranspileContext.

Trait Implementations

impl<'a> Debug for LogicExpr<'a>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'a> DisplayWith for LogicExpr<'a>

fn fmt_with( &self, interner: &Interner, f: &mut Formatter<'_>, ) -> Result<(), Error>

fn with<'a>(&'a self, interner: &'a Interner) -> WithInterner<'a, Self>

impl<'a, 'b> Resolve<'a> for LogicExpr<'b>

type Output = ExprView<'a>

fn resolve(&self, interner: &'a Interner) -> ExprView<'a>