In this post we give the Haskell code for a lambda calculus in which the variables are locations in lambda terms. This is a very generic procedure. Given a polynomial bi-functor, M[V,A], we can form the type M[(∂µMxµM),µM]. When M is really a nominal algebra this results in algebraic terms in which names are really positions in terms. This is another milestone along the way to providing a rational reconstruction of geometry in which geometry arises from computational behavior.

module Generators(

Term

, MuTerm

, DoTerm

, ReflectiveTerm

, TermLocation

, ClosedTermLocation

, ClosedReflectiveTerm

, unfoldLocation

, unfoldTerm

, makeMention

, makeAbstraction

, makeApplication

, generateTerms

)

where

-- M[V,A] = 1 + V + VxA + AxA

data Term v a =

Divergence

| Mention v

| Abstraction v a

| Application a a

deriving (Eq, Show)

-- μ M

data MuTerm v = MuTerm (Term v (MuTerm v)) deriving (Eq, Show)

-- ∂μ M

data DoTerm v =

Hole

| DoAbstraction v (DoTerm v)

| DoLeftApplication (DoTerm v) (MuTerm v)

| DoRightApplication (MuTerm v) (DoTerm v)

deriving (Eq, Show)

-- first trampoline

data ReflectiveTerm v = ReflectiveTerm (MuTerm (DoTerm v, ReflectiveTerm v))

deriving (Eq, Show)

-- second trampoline

data TermLocation v = TermLocation ((DoTerm v), (ReflectiveTerm v))

deriving (Eq, Show)

-- first bounce

data ClosedTermLocation = ClosedTermLocation (TermLocation ClosedTermLocation)

deriving (Eq, Show)

-- second bounce

data ClosedReflectiveTerm =

ClosedReflectiveTerm (ReflectiveTerm ClosedTermLocation)

deriving (Eq, Show)

-- the isomorphisms implied by the trampolines

unfoldLocation ::

ClosedTermLocation

-> ((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation))

unfoldLocation (ClosedTermLocation (TermLocation (k, t))) = (k, t)

unfoldTerm ::

ClosedReflectiveTerm

-> (MuTerm

((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation)))

unfoldTerm (ClosedReflectiveTerm (ReflectiveTerm muT)) = muT

-- variable mention ctor

makeMention :: ClosedTermLocation -> ClosedReflectiveTerm

makeMention ctl =

(ClosedReflectiveTerm

(ReflectiveTerm (MuTerm (Mention (unfoldLocation ctl)))))

-- abstraction ctor

makeAbstraction ::

ClosedTermLocation -> ClosedReflectiveTerm -> ClosedReflectiveTerm

makeAbstraction ctl crt =

(ClosedReflectiveTerm

(ReflectiveTerm

(MuTerm

(Abstraction

(unfoldLocation ctl)

(unfoldTerm crt)))))

-- application ctor

makeApplication ::

ClosedReflectiveTerm -> ClosedReflectiveTerm -> ClosedReflectiveTerm

makeApplication crtApplicad crtApplicand =

(ClosedReflectiveTerm

(ReflectiveTerm

(MuTerm

(Application

(unfoldTerm crtApplicad)

(unfoldTerm crtApplicand)))))

-- a simple test

generateTerms :: () -> [ClosedReflectiveTerm]

generateTerms () =

-- x

[(makeMention

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))),

-- \x -> x

(makeAbstraction

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))

(makeMention

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))),

-- ((\x -> x)(\x -> x))

(makeApplication

(makeAbstraction

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))

(makeMention

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))))

(makeAbstraction

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))

(makeMention

(ClosedTermLocation

(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))))]

## No comments:

Post a Comment