lambda-sampler-1.1: Boltzmann sampler utilities for lambda calculus.

Data.Lambda

Contents

Description

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.

Synopsis

Lambda terms

data Lambda Source #

Lambda terms with de Bruijn indices.

Constructors

 Var Index de Bruijn indices. Abs Lambda Lambda abstraction. App Lambda Lambda Term application.

Instances

 Source # MethodsshowsPrec :: Int -> Lambda -> ShowS #showList :: [Lambda] -> ShowS #

Predicate defining closed lambda terms.

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.

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

Finds the maximal index in the given lambda term.

de Bruijn indices

data Index Source #

de Bruijn indices in unary notation.

Constructors

 S Index Z

Instances

 Source # MethodsshowsPrec :: Int -> Index -> ShowS #show :: Index -> String #showList :: [Index] -> ShowS #

toInt :: Num a => Index -> a Source #

Translates the given index to a corresponding positive integer.

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

Translates the given positive integer to a corresponding index.