License	GPL-3
Safe Haskell	Safe

NamedLambda

Description

This package deals with lambda expressions containing named variables instead of DeBruijn indexes. It contains parsing and printing fuctions.

Synopsis

Documentation

data NamedLambda Source #

A lambda expression with named variables.

Constructors

LambdaVariable String	variable
LambdaAbstraction String NamedLambda	lambda abstraction
LambdaApplication NamedLambda NamedLambda	function application
TypedPair NamedLambda NamedLambda	pair of expressions
TypedPi1 NamedLambda	first projection
TypedPi2 NamedLambda	second projection
TypedInl NamedLambda	left injection
TypedInr NamedLambda	right injection
TypedCase NamedLambda NamedLambda NamedLambda	case of expressions
TypedUnit	unit
TypedAbort NamedLambda	abort
TypedAbsurd NamedLambda	absurd

Instances

Eq NamedLambda Source #
Methods (==) :: NamedLambda -> NamedLambda -> Bool (/=) :: NamedLambda -> NamedLambda -> Bool
Show NamedLambda Source #
Methods showsPrec :: Int -> NamedLambda -> ShowS show :: NamedLambda -> String showList :: [NamedLambda] -> ShowS

lambdaexp :: Parser NamedLambda Source #

Parses a lambda expression with named variables. A lambda expression is a sequence of one or more autonomous lambda expressions. They are parsed assuming left-associativity.

>>> parse lambdaexp "" "\\f.\\x.f x"
Right λf.λx.(f x)

Note that double backslashes are neccessary only when we quote strings; it will work only with a simple backslash in the interpreter.

toBruijn Source #

Arguments

:: Context	Variable context
-> NamedLambda	Initial lambda expression with named variables
-> Exp

Transforms a lambda expression with named variables to a deBruijn index expression. Uses only the dictionary of the variables in the current context.

nameExp :: Exp -> NamedLambda Source #

Gives names to every variable in a deBruijn expression using alphabetic order.

quicknameIndexes :: Int -> [String] -> Exp -> NamedLambda Source #

variableNames :: [String] Source #

A list of all possible variable names in lexicographical order.