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