Tuesday, July 20, 2010


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(
, MuTerm
, DoTerm
, ReflectiveTerm
, TermLocation
, ClosedTermLocation
, ClosedReflectiveTerm
, unfoldLocation
, unfoldTerm
, makeMention
, makeAbstraction
, makeApplication
, generateTerms

-- M[V,A] = 1 + V + VxA + AxA
data Term v a =
| 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 =
| 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 ::
-> ((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation))

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

unfoldTerm ::
-> (MuTerm
((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation)))

unfoldTerm (ClosedReflectiveTerm (ReflectiveTerm muT)) = muT

-- variable mention ctor
makeMention :: ClosedTermLocation -> ClosedReflectiveTerm

makeMention ctl =
(ReflectiveTerm (MuTerm (Mention (unfoldLocation ctl)))))

-- abstraction ctor
makeAbstraction ::
ClosedTermLocation -> ClosedReflectiveTerm -> ClosedReflectiveTerm

makeAbstraction ctl crt =
(unfoldLocation ctl)
(unfoldTerm crt)))))

-- application ctor
makeApplication ::
ClosedReflectiveTerm -> ClosedReflectiveTerm -> ClosedReflectiveTerm

makeApplication crtApplicad crtApplicand =
(unfoldTerm crtApplicad)
(unfoldTerm crtApplicand)))))

-- a simple test
generateTerms :: () -> [ClosedReflectiveTerm]

generateTerms () =
-- x
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))),
-- \x -> x
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))),
-- ((\x -> x)(\x -> x))
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))))
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))
(TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))))]

No comments: