[Haskell-cafe] lambda terms in which the variables are positions in lambda terms

21 Jul 2010

      Dear Haskellians,

The following code may provide some amusement. i offer a free copy of
Barwise's Vicious Circles to the first person to derive deBruijn indices
from this presentation.

Best wishes,

--greg

-- -*- mode: Haskell;-*-
-- Filename:    Term.hs
-- Authors:     lgm
-- Creation:    Tue Jul 20 16:37:37 2010
-- Copyright:   Not supplied
-- Description:
-- ------------------------------------------------------------------------

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)

-- \mu M
data MuTerm v = MuTerm (Term v (MuTerm v)) deriving (Eq, Show)

-- \partial \mu 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)))))))]

-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com

[Haskell-cafe] lambda terms in which the variables are positions in lambda terms

Greg Meredith