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:

$3

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.

$3

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

$3

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

$3

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

$3

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

$3

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

Usage Examples

$3

`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);
`

$3


`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. We are particularly grateful for their clear implementation of operator precedence and formula evaluation, which served as a model for our TypeScript adaptation.