Data.Lambda

Lambda terms in the de Bruijn notation where instead of variables, we use natural indices encoded as a sequence of successors of zero.

Each index captures the distance to its binding lambda - Z corresponds to a variable bound by the first lambda abstraction on its way to the term root. The successor S increases the distance of its argument by one. If an index points to a lambda abstraction outside of the term, then that index represents a free variable in the term. Such a representation for lambda terms avoids using explicit variable names and hence eliminates the use of alpha-conversion.

Lambda terms

data Lambda

Lambda terms with de Bruijn indices.

Constructors

Var Index

de Bruijn indices.

Abs Lambda

Lambda abstraction.

App Lambda Lambda

Term application.

Instances

Show Lambda

Methods

showsPrec :: Int -> Lambda -> ShowS

show :: Lambda -> String

showList :: [Lambda] -> ShowS

isClosed :: Lambda -> Bool

Predicate defining closed lambda terms.

size

Arguments

:: Num a

=> Model a

Size notion used in the computations.

-> Lambda

The considered lambda term.

-> a

The integer size of the lambda term.

Computes the size of the given lambda term.

sizeVar

Arguments

:: Num a

=> Model a

Size notion used in the computations.

-> Index

The considered de Bruijn index.

-> a

The integer size of the lambda term.

Computes the size of the given de Bruijn index.

maxIndex :: (Num a, Ord a) => Lambda -> a

Finds the maximal index in the given lambda term.

de Bruijn indices

data Index

de Bruijn indices in unary notation.

Constructors

S Index

Z

Instances

Show Index

Methods

showsPrec :: Int -> Index -> ShowS

show :: Index -> String

showList :: [Index] -> ShowS

toInt :: Num a => Index -> a

Translates the given index to a corresponding positive integer.

toIndex :: (Num a, Eq a) => a -> Index

Translates the given positive integer to a corresponding index.