tfl-js

This library is a TypeScript reimplementation of the propositional logic components from the Carnap project, specifically focusing on formula parsing and evaluation. While Carnap is a comprehensive logic education platform written in Haskell, this library extracts and modernizes the core propositional logic functionality for use in JavaScript/TypeScript environments.

Learning from Carnap

Our TypeScript implementation draws several key insights from Carnap's Haskell codebase:

Operator Precedence

One of the most important lessons from Carnap was its handling of operator precedence. In Carnap's Parser.hs, precedence is defined explicitly:

standardOpTable = [ [ Prefix (try parseNeg)]
                  , [Infix (try parseOr) AssocLeft, Infix (try parseAnd) AssocLeft]
                  , [Infix (try parseIf) AssocNone, Infix (try parseIff) AssocNone]
                  ]

We adapted this in our TypeScript implementation using Chevrotain's grammar rules:

// Highest precedence: Negation
private negation = this.RULE("negation", () => {
  this.OPTION(() => this.CONSUME(Tokens.StandardNot));
  this.SUBRULE(this.primary);
});

// Higher precedence: Conjunction
private conjunction = this.RULE("conjunction", () => {
  this.SUBRULE(this.negation);
  this.MANY(() => {
    this.CONSUME(Tokens.StandardAnd);
    this.SUBRULE2(this.negation);
  });
});

// Middle precedence: Disjunction
private disjunction = this.RULE("disjunction", () => {
  this.SUBRULE(this.conjunction);
  this.MANY(() => {
    this.CONSUME(Tokens.StandardOr);
    this.SUBRULE2(this.conjunction);
  });
});

// Lowest precedence: Implications
private implication = this.RULE("implication", () => {
  this.SUBRULE(this.disjunction);
  this.MANY(() => {
    this.CONSUME(Tokens.StandardIf);
    this.SUBRULE2(this.disjunction);
  });
});

This ensures that formulas like p ∨ q ∧ r are correctly parsed as p ∨ (q ∧ r), matching Carnap's behavior.

Formula Representation

Carnap uses algebraic data types to represent formulas:

data PureForm = Atomic String
              | Negation PureForm
              | Conjunction PureForm PureForm
              | Disjunction PureForm PureForm
              | Conditional PureForm PureForm
              | Biconditional PureForm PureForm

We adapted this using TypeScript's type system:

interface Formula {
  evaluate(valuation: Valuation): boolean;
  subformulas(): Formula[];
  atoms(): string[];
}

class Atom implements Formula {
  constructor(public readonly name: string) {}
  // Implementation...
}

class Compound implements Formula {
  constructor(
    public readonly operator: Operator,
    public readonly left: Formula,
    public readonly right?: Formula
  ) {}
  // Implementation...
}

Key differences:

• Uses interfaces and classes instead of algebraic data types
• Implements visitor pattern through method dispatch
• Provides stronger type safety through TypeScript's type system

Parser Architecture

While Carnap uses Parsec for parsing, we chose Chevrotain for several reasons:

1. Better error recovery and reporting
2. More natural fit for JavaScript/TypeScript
3. Explicit separation of lexing and parsing phases

Our parser maintains Carnap's key features:

• Multiple notation styles (standard, TFL, English)
• Proper operator precedence
• Comprehensive error handling

Formula Evaluation

Carnap's evaluation strategy is based on Haskell's type classes. We adapted this to a more object-oriented approach:

class Evaluator {
  isTautology(formula: Formula): boolean {
    const atoms = formula.atoms();
    const valuations = this.generateValuations(atoms);
    return valuations.every(v => formula.evaluate(v));
  }

  isContradiction(formula: Formula): boolean {
    const atoms = formula.atoms();
    const valuations = this.generateValuations(atoms);
    return valuations.every(v => !formula.evaluate(v));
  }

  // More evaluation methods...
}

Key improvements:

• Efficient bit operations for valuation generation
• Direct access to evaluation results
• Clearer error messages

Implementation Status

✅ Completed Features

Core Types

• [x] Formula type system with interfaces and base classes
• [x] Atomic proposition representation
• [x] Compound formula representation with operators
• [x] Type-safe formula construction
• [x] Formula evaluation interface

Parser Implementation

• [x] Lexer for tokenizing input
  • Supports standard notation (¬, ∧, ∨, →, ↔)
  • Supports TFL notation (~, &, v, ->, <->)
  • Supports English notation (not, and, or, if, iff)
• [x] Recursive descent parser using Chevrotain
• [x] Proper operator precedence handling
• [x] Support for parentheses and nested expressions
• [x] Comprehensive error handling with position information
• [x] Enhanced sequent parser
  • Support for empty premises (⊨ C)
  • Multiple turnstile symbols (⊨, ⊢, |-)
  • Robust whitespace handling
  • Comprehensive error handling

Formula Evaluation

• [x] Basic formula evaluation
• [x] Tautology checking
• [x] Contradiction checking
• [x] Contingency checking
• [x] Logical equivalence
• [x] Valid consequence checking
• [x] Satisfying valuation finding

Error Handling

• [x] Base error class hierarchy
• [x] Detailed parsing errors with position tracking
• [x] Evaluation and validation error types
• [x] User-friendly error messages

🚧 In Progress

• [ ] Formula manipulation utilities
• [ ] Documentation and examples

Usage Examples

Basic Formula Evaluation

const parser = new TFLParser();
const evaluator = new Evaluator();

// Parse and evaluate a formula
const formula = parser.parse('p ∧ (q → r)');
const result = formula.evaluate({ p: true, q: false, r: true });

// Check formula properties
const isTaut = evaluator.isTautology(formula);
const isContrad = evaluator.isContradiction(formula);
const isConting = evaluator.isContingent(formula);

// Find satisfying valuations
const satisfying = evaluator.findSatisfyingValuations(formula);

// Check logical equivalence
const f1 = parser.parse('p → q');
const f2 = parser.parse('¬p ∨ q');
const areEquiv = evaluator.areEquivalent(f1, f2);

Error Handling

try {
  parser.parse('p ∧ (q → ');
} catch (error) {
  if (error instanceof ParseError) {
    console.log(error.toString());
    // Output: ParseError at line 1, column 8: Expected ")"
    // p ∧ (q →
    //        ^
  }
}

Project Structure

tfl-js/
├── src/
│   ├── types/
│   │   └── formula.ts    # Core formula types
│   ├── parser/
│   │   ├── lexer.ts      # Token definitions and lexer
│   │   └── parser.ts     # Parser implementation
│   ├── evaluator/
│   │   └── index.ts      # Formula evaluation engine
│   └── errors/
│       └── index.ts      # Error types
├── tests/
│   ├── parser/
│   │   ├── lexer.test.ts # Lexer tests
│   │   └── parser.test.ts # Parser tests
│   └── evaluator/
│       └── evaluator.test.ts # Evaluator tests

Getting Started

# Install dependencies
bun install

# Run tests
bun test

# Build package
bun run build

Acknowledgments

This library is a TypeScript reimplementation of the propositional logic components from the Carnap project. We are particularly grateful for their clear implementation of operator precedence and formula evaluation, which served as a model for our TypeScript adaptation.