Implementations of various lambda calculus based systems. Source code Contents Index

Typed.Calculus Stability experimental Maintainer thanos@sians.org

Contents Data types Evaluator Evaluation methods Term predicates

Description

Calculus for the typed system.

Synopsis

type Computation = [Term] type Computer = Term -> Computation eval1 :: Term -> Term compute :: Computer safecompute :: Computer bigstep :: Computer -> Term -> Term canStep :: Term -> Bool isStuck :: Term -> Bool

Data types

type Computation = [Term] Source

List of terms that represents a computation.

type Computer = Term -> Computation Source

A computer takes a term and returns the term's computation.

Evaluator

eval1 :: Term -> Term Source

Small-step evaluation. Operational semantics for this calculus.

Evaluation methods

compute :: Computer Source

Step-by-step evaluation. It may easily loop infinitely.

safecompute :: Computer Source

Step-by-step safe evaluation, avoiding easy-to-catch loops.

bigstep :: Computer -> Term -> Term Source

Transforms a Computer into a big-step evaluator.

Term predicates

canStep :: Term -> Bool Source

Checks if the given term can make a computational step.

isStuck :: Term -> Bool Source

A term that cannot take any step, but still is not a value.

Produced by Haddock version 2.4.2