Softwhere

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)))))))]