# 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:

```haskell
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:

```typescript
// 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:

```haskell
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:

```typescript
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:

```typescript
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
```typescript
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
```typescript
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

```bash
# 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](https://carnap.io/). We are particularly grateful for their clear implementation of operator precedence and formula evaluation, which served as a model for our TypeScript adaptation.