lambda_calculus 1.3.0

A library for lambda calculus. It supports parsing and evaluating lambda terms with different strategies. It also has preliminary support for type inference.

lamdba-calculus

Introduction

A Lambda Calculus parser & evaluator in dart.

Use import 'package:lambda_calculus/lambda_calculus.dart'; to use this library.

Currently, it supports evaluating untyped Lambda Calculus as well as type inference.

Check out the quickstart for a quick usage guide.

If you notice any issues or have any suggestions, please feel free to open an issue or contact me via email.

Quickstart

import 'package:lambda_calculus/lambda_calculus.dart';

// Parse a lambda expression
// the lambda character 'λ' can be replaced by '/' or '\' for convenience;
final yCombinator = r'/x. (\y -> x (\z. y y z)) (/y. x (/z. y y z))'.toLambda()!;
// The output tries its best to preserve the variable names.
print(yCombinator);

// Church numbers
final fortyTwo = 42.toChurchNumber();
final iiyokoiyo = 114514.toChurchNumber(); // I wouldn't try to print out this one...

// Evaluate a lambda expression
// Note that we use `LambdaBuilder` to constructor lambda expressions bottom-up.
// We need to call the `build` method at the end to get the final lambda
// expression.
// Both `LambdaBuilder` and `Lambda` provides a number of constants and
// combinators for convenience.
final twoTimesThree = LambdaBuilder.applyAll([
  LambdaBuilder.constants.lambdaTimes(),
  2.toChurchNumberBuilder(),
  3.toChurchNumberBuilder(),
]).build();
final evalOneStep = twoTimesThree.eval1();
// Note that the 'eval' function does not terminate if the term does not have
// a normal form.
final callByValueResult = twoTimesThree.eval();
final callByNameResult = twoTimesThree.eval(LambdaEvaluationType.callByName);
final fullReductionResult = twoTimesThree.eval(LambdaEvaluationType.fullReduction);
print(fullReductionResult); // Same as `LambdaConstants.six()` or `6.toChurchNumber()`

// Find the type of a lambda expression;
final term = r'\x. \y. x y'.toLambda()!;
print(term.findType()); // (t1 -> t2) -> (t1 -> t2)
// The Y-combinator has no type under the Hindley-Milner type system
print(yCombinator.findType()); // null

See here for more examples.