Crate logicaffeine_kernel 

The Kernel: Calculus of Constructions

A unified type system where terms and types are the same syntactic category, based on the Calculus of Inductive Constructions (CIC).

Core Insight

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

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│
└───────────────┘ └───────────────┘ └───────────────┘ └───────────┘

Public API

Core Types

• Term - The unified representation of terms, types, and proofs
• Context - Typing context with local and global bindings
• KernelError - Error types for type checking failures

Type Checking

• infer_type - Infer the type of a term
• is_subtype - Check subtyping with cumulativity
• normalize - Reduce a term to normal form

Decision Procedures

• ring - Polynomial equality by normalization
• lia - Linear arithmetic by Fourier-Motzkin
• cc - Congruence closure for uninterpreted functions
• omega - Integer arithmetic with exact semantics
• simp - General simplification with rewriting

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.

Modules

cc

Congruence Closure Tactic

interface

Vernacular interface for the Kernel.

lia

LIA Tactic: Linear Integer Arithmetic by Fourier-Motzkin Elimination

omega

Omega Test: True Integer Arithmetic Decision Procedure

positivity

Strict positivity checking for inductive types.

prelude

Standard Library for the Kernel.

ring

Ring Tactic: Polynomial Equality by Normalization

simp

Simplifier Tactic

termination

Termination checking for fixpoints.

Structs

Context

Typing context: maps variable names to their types.

Enums

KernelError

Errors that can occur during type checking.

Literal

Primitive literal values.

Term

Unified term representation.

Universe

Universe levels in the type hierarchy.

Functions

infer_type

Infer the type of a term in a context.

is_subtype

Check if type a is a subtype of type b (cumulativity).

normalize

Normalize a term to its normal form.

Type Aliases

KernelResult

Result type for kernel operations.