logicaffeine-kernel

Pure Calculus of Constructions (CoC) type theory implementation. This is the logical kernel for Logicaffeine—a language-agnostic type checker and proof assistant core.

Overview

The kernel implements the Calculus of Inductive Constructions, a unified type system where terms and types inhabit the same syntactic category. Everything is a Term:

• Types are Terms: Nat : Type 0
• Values are Terms: zero : Nat
• Functions are Terms: λx:Nat. x
• Proofs are Terms: refl : a = a

Milner Invariant

This crate has no path to the lexicon. Adding words to the English vocabulary never triggers a recompile of the type checker. The kernel is purely logical and language-agnostic.

Natural Language → Lexer → Parser → Compile → Kernel
                                                 ↑
                                   (no lexicon dependency)

Core Types

Term

The unified representation for all expressions:

pub enum Term {
    Sort(Universe),       // Type 0, Type 1, Prop
    Var(String),          // Local variable
    Global(String),       // Global definition
    Pi { ... },           // Π(x:A). B (dependent function type)
    Lambda { ... },       // λ(x:A). t (function)
    App(Box<Term>, Box<Term>),  // f x (application)
    Match { ... },        // Pattern matching
    Fix { ... },          // Recursive fixpoint
    Lit(Literal),         // i64, f64, String
    Hole,                 // Implicit argument
}

Universe

The type hierarchy: Prop : Type 1 : Type 2 : ...

pub enum Universe {
    Prop,      // Propositions (proof-irrelevant)
    Type(u32), // Types at level n
}

Universe subtyping (cumulativity):

• Prop ≤ Type(i) for all i
• Type(i) ≤ Type(j) if i ≤ j

Context

Typing context with three kinds of bindings:

• Inductives: Type definitions (Nat : Type 0)
• Constructors: Data constructors (Zero : Nat, Succ : Nat → Nat)
• Definitions: Named terms with their types

Public API

Type Checking

use logicaffeine_kernel::{Context, Term, infer_type, is_subtype, normalize};

let ctx = Context::new();

// Infer the type of a term
let ty = infer_type(&ctx, &term)?;

// Check subtyping with cumulativity
let sub = is_subtype(&ctx, &term_a, &term_b)?;

// Reduce to normal form
let nf = normalize(&ctx, &term);

Standard Library

use logicaffeine_kernel::prelude::StandardLibrary;

let mut ctx = Context::new();
StandardLibrary::register(&mut ctx);
// Now ctx has: Entity, Nat, Bool, True, False, Not, Eq, And, Or, Ex, Int, Float, Text

Standard types:

Decision Procedures

The kernel includes automated proof tactics:

The try_auto tactic tries all procedures in sequence: simp → ring → cc → omega → lia.

Reflection System

Deep embedding for metaprogramming with Syntax (quoted terms) and Derivation (proof trees):

Syntax constructors:
  SVar, SGlobal, SSort, SApp, SLam, SPi, SLit, SName

Derivation constructors:
  DAxiom, DModusPonens, DUnivIntro, DUnivElim, DRefl, DInduction,
  DCompute, DCong, DElim, DInversion, DRewrite, DDestruct, DApply

Operations: syn_size, syn_max_var, syn_lift, syn_subst, syn_beta, syn_step, syn_eval, syn_quote, syn_diag.

Architecture

┌─────────────────────────────────────────────────────────────┐
│                        Interface                            │
│  (term_parser, literate_parser, command)                    │
└─────────────────────────────────────────────────────────────┘
                             │
                             ▼
┌─────────────────────────────────────────────────────────────┐
│                      Type Checker                           │
│  infer_type, is_subtype, substitute                         │
└─────────────────────────────────────────────────────────────┘
                             │
              ┌──────────────┴──────────────┐
              ▼                             ▼
┌─────────────────────────┐   ┌─────────────────────────────┐
│      Reduction          │   │         Prelude             │
│  normalize, reduce      │   │  standard library types     │
└─────────────────────────┘   └─────────────────────────────┘
                                            │
              ┌─────────────┬───────────────┼───────────────┐
              ▼             ▼               ▼               ▼
┌───────────────┐ ┌───────────────┐ ┌───────────────┐ ┌───────────┐
│     ring      │ │     lia       │ │      cc       │ │   omega   │
│  polynomial   │ │    linear     │ │  congruence   │ │  integer  │
│   equality    │ │  arithmetic   │ │   closure     │ │ arithmetic│
└───────────────┘ └───────────────┘ └───────────────┘ └───────────┘

Directory Structure

src/
├── lib.rs              # Crate root, public exports
├── term.rs             # Term, Universe, Literal types
├── context.rs          # Typing context with bindings
├── type_checker.rs     # Type inference and subtyping
├── reduction.rs        # Normalization and reduction
├── error.rs            # KernelError, KernelResult
├── ring.rs             # Ring decision procedure
├── lia.rs              # Linear integer arithmetic (Fourier-Motzkin)
├── cc.rs               # Congruence closure
├── omega.rs            # Integer arithmetic with floor/ceil
├── simp.rs             # Rewriting simplification
├── prelude.rs          # Standard library definitions
├── positivity.rs       # Strict positivity checking for inductives
├── termination.rs      # Termination checking for Fix
└── interface/          # REPL, parsing, literate syntax

License

Business Source License 1.1 (BUSL-1.1)

• Free for individuals and organizations with <25 employees
• Commercial license required for organizations with 25+ employees offering Logic Services
• Converts to MIT on December 24, 2029

See LICENSE for full terms.