Dear Haskellians,<div><br></div><div>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.</div><div><br>
</div><div>Best wishes,</div><div><br></div><div>--greg</div><div><br></div><div><div>-- -*- mode: Haskell;-*- </div><div>-- Filename: Term.hs </div><div>-- Authors: lgm </div>
<div>-- Creation: Tue Jul 20 16:37:37 2010 </div><div>-- Copyright: Not supplied </div><div>-- Description: </div><div>-- ------------------------------------------------------------------------</div><div><br></div><div>
module Generators(</div><div> Term</div><div> , MuTerm</div><div> , DoTerm</div><div> , ReflectiveTerm</div><div> , TermLocation</div><div>
, ClosedTermLocation</div><div> , ClosedReflectiveTerm</div><div> , unfoldLocation</div><div> , unfoldTerm</div><div> , makeMention</div>
<div> , makeAbstraction</div><div> , makeApplication</div><div> , generateTerms</div><div> )</div><div> where</div><div><br></div><div>-- M[V,A] = 1 + V + VxA + AxA</div>
<div>data Term v a =</div><div> Divergence</div><div> | Mention v</div><div> | Abstraction v a</div><div> | Application a a</div><div> deriving (Eq, Show)</div><div><br></div><div>-- \mu M</div><div>
data MuTerm v = MuTerm (Term v (MuTerm v)) deriving (Eq, Show)</div><div><br></div><div>-- \partial \mu M</div><div>data DoTerm v = </div><div> Hole</div><div> | DoAbstraction v (DoTerm v)</div><div> | DoLeftApplication (DoTerm v) (MuTerm v)</div>
<div> | DoRightApplication (MuTerm v) (DoTerm v)</div><div> deriving (Eq, Show)</div><div><br></div><div>-- first trampoline</div><div>data ReflectiveTerm v = ReflectiveTerm (MuTerm (DoTerm v, ReflectiveTerm v))</div>
<div> deriving (Eq, Show)</div><div><br></div><div>-- second trampoline</div><div>data TermLocation v = TermLocation ((DoTerm v), (ReflectiveTerm v))</div><div> deriving (Eq, Show)</div>
<div><br></div><div>-- first bounce</div><div>data ClosedTermLocation = ClosedTermLocation (TermLocation ClosedTermLocation)</div><div> deriving (Eq, Show)</div><div><br></div><div>-- second bounce</div>
<div>data ClosedReflectiveTerm =</div><div> ClosedReflectiveTerm (ReflectiveTerm ClosedTermLocation)</div><div> deriving (Eq, Show)</div><div><br></div><div>-- the isomorphisms implied by the trampolines</div><div>unfoldLocation ::</div>
<div> ClosedTermLocation</div><div> -> ((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation))</div><div><br></div><div>unfoldLocation (ClosedTermLocation (TermLocation (k, t))) = (k, t)</div><div>
<br></div><div>unfoldTerm ::</div><div> ClosedReflectiveTerm</div><div> -> (MuTerm</div><div> ((DoTerm ClosedTermLocation), (ReflectiveTerm ClosedTermLocation)))</div><div><br></div><div>unfoldTerm (ClosedReflectiveTerm (ReflectiveTerm muT)) = muT</div>
<div><br></div><div>-- variable mention ctor</div><div>makeMention :: ClosedTermLocation -> ClosedReflectiveTerm</div><div><br></div><div>makeMention ctl =</div><div> (ClosedReflectiveTerm</div><div> (ReflectiveTerm (MuTerm (Mention (unfoldLocation ctl)))))</div>
<div><br></div><div>-- abstraction ctor</div><div>makeAbstraction ::</div><div> ClosedTermLocation -> ClosedReflectiveTerm -> ClosedReflectiveTerm</div><div> </div><div>makeAbstraction ctl crt =</div>
<div> (ClosedReflectiveTerm</div><div> (ReflectiveTerm</div><div> (MuTerm</div><div> (Abstraction</div><div> (unfoldLocation ctl)</div><div> (unfoldTerm crt)))))</div><div><br></div><div>-- application ctor</div>
<div>makeApplication ::</div><div> ClosedReflectiveTerm -> ClosedReflectiveTerm -> ClosedReflectiveTerm</div><div><br></div><div>makeApplication crtApplicad crtApplicand =</div><div> (ClosedReflectiveTerm</div>
<div> (ReflectiveTerm</div><div> (MuTerm</div><div> (Application</div><div> (unfoldTerm crtApplicad)</div><div> (unfoldTerm crtApplicand)))))</div><div><br></div><div>-- a simple test</div><div>
generateTerms :: () -> [ClosedReflectiveTerm]</div><div><br></div><div>generateTerms () =</div><div> -- x</div><div> [(makeMention </div><div> (ClosedTermLocation</div><div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))),</div>
<div> -- \x -> x</div><div> (makeAbstraction</div><div> (ClosedTermLocation</div><div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))</div><div> (makeMention</div><div> (ClosedTermLocation</div>
<div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))),</div><div> -- ((\x -> x)(\x -> x))</div><div> (makeApplication</div><div> (makeAbstraction</div><div> (ClosedTermLocation</div>
<div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))</div><div> (makeMention</div><div> (ClosedTermLocation</div><div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))))</div>
<div> (makeAbstraction</div><div> (ClosedTermLocation</div><div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence))))</div><div> (makeMention</div><div> (ClosedTermLocation</div><div> (TermLocation (Hole, ReflectiveTerm (MuTerm Divergence)))))))]</div>
<br>-- <br>L.G. Meredith<br>Managing Partner<br>Biosimilarity LLC<br>1219 NW 83rd St <br>Seattle, WA 98117<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com">http://biosimilarity.blogspot.com</a><br>
</div>