Binary Tree Arithmetic with Generalized Constructors Abstract whilekeepingthePeanoarithmeticviewwhenmoreconvenientin proofs [9]. Note also that free algebras corresponding to one and We describe arithmetic computations in terms of operations on 3 twosuccessorarithmetic(S1SandS2S)havebeenusedasabasis some well known free algebras (S1S, S2S and ordered rooted 1 fordecidableweakarithmeticsystemslike[2]and[11].Ithasbeen binary trees) while emphasizing the common structure present in 0 shownrecentlyin[16,17]thattheinitialalgebraoforderedrooted allthemwhenseenasisomorphicwiththesetofnaturalnumbers. 2 binary trees corresponding to the language of Go¨del’s System T Constructorsanddeconstructorsseenthroughaninitialalgebra types [7] can be used as a the language of arithmetic representa- n semanticsaregeneralizedtorecursivelydefinedfunctionsobeying tions, with hyper-exponential gains when handling numbers built Ja sairmeidlaisrcluaswsesd. ItmogpelethmeernwtaittihonasnuaspinpglicSactiaolan’stoapaprleyaliasntidcuanrbaiptrpalryy from“towersofexponents”like22...2.Independently,thisviewis sizearithmeticpackagewritteninScala,basedonthefreealgebra confirmedbythesuggestiontouseλ-termsasaformofuniversal 1 ofrootedorderedbinarytrees,whichalsosupportsrationalnumber data compression tool [8] and by deriving bijective encodings of operationsthroughanextensiontosignedrationalsoftheCalkin- datatypesusingagame-basedmechanism[18]. ] S Wilfbijection. These results suggest a free algebra based reconstruction of M fundamental data types that are relevant as building blocks for Categories and Subject Descriptors D.3.3 [PROGRAMMING finite mathematics and computer science. We will sketch in this LANGUAGES]: Language Constructs and Features—Data types . paperan(elementary,notinvolvingcategorytheory)foundationfor s andstructures c arithmeticcomputationswithfreealgebras,inwhichconstruction [ GeneralTerms Algorithms,Languages,Theory ofsets,sequences,graphs,etc.canbefurthercarriedoutalongthe Keywords arithmetic computations with free algebras, general- linesof[14,15,17]. 1 Thepaperisorganizedasfollows.Wedefineinsection2iso- izedconstructors,declarativemodelingofcomputationalphenom- v morphisms between the free algebras of signatures consisting of ena,bijectiveGo¨delnumberingsandalgebraicdatatypes,Calkin- 8 oneconstantandrespectively,ofonesuccessor(S),twosuccessors Wilfbijectionbetweennaturalandrationalnumbers 2 (OandI)andafreemagmaconstructor(C). 1 To enable computations with the objects of the free algebras, 1. Introduction 0 wediscusstheuseofgeneralizedconstructors/destructorsderived 1. Classicalmathematicsfrequentlyusesfunctionsdefinedonequiv- fromthesefreealgebrasusingtheapply/unapplyconstructsavail- alenceclasses(e.g.modulararithmetic,factorobjectsinalgebraic able in Scala (section 3). As an application, a complete arbitrary 0 structures)providedthatitcanprovethatthechoiceofarepresen- sizerationalarithmeticpackageusingtheCalkin-Wilfbijectionbe- 3 tativeintheclassisirrelevant. tweenpositiverationalsandnaturalnumbersisdescribedinsection 1 On the other hand, when working with proof assistants like 4.Sections5and6discussrelatedworkandourconclusions. : v Coq [9], based on type theory and its computationally refined Xi extensionsliketheCalculusofConstruction[4],onecannotavoid 2. FreeAlgebrasandDataTypes noticingtheprevalenceofdatatypescorrespondingtofreeobjects, r on top of which everything else is built in the form of canonical DEFINITION1. Letσ beasignatureconsistingofanalphabetof a representations. constants(calledgenerators)andanalphabetoffunctionsymbols Category-theorybaseddescriptionsofPeanoarithmeticfitnat- (calledconstructors)withvariousarities.Wedefinethefreealgebra urallyinthegeneralviewthatdatatypesareinitialalgebras-in Aσofsignatureσinductivelyasthesmallestsetsuchthat: thiscasetheinitialalgebrageneratedbythesuccessorfunction,as 1. ifcisaconstantofσthenc∈A aproviderofthecanonicalrepresentationofnaturalnumbers.Of σ 2. iff isann-argumentfunctionsymbolofσ,then∀i,0 ≤ i < course,acriticalelementinchoosingsuchfreealgebrasiscompu- n,t ∈A ⇒f(t ,...,t ,...,t )∈A . tationalefficiencyoftheoperationsonewantstoperformonthem, i σ 0 i n−1 σ intermsoflowtimeandspacecomplexity.ForinstanceCoqfor- Wewillwritec/0forconstantsandf/nforfunctionsymbolswith malizationsofnaturalnumberstypicallyusebinaryrepresentations nargumentsbelongingtoagivenasignature. Moregeneraldefinitions,e.g.asinitialobjectsinthecategoryof algebraicstructures,arealsousedintheliteratureandacloserela- tionexistswithtermalgebrasdistinguishingbetweenfunctioncon- Permissiontomakedigitalorhardcopiesofallorpartofthisworkforpersonalor structors (generating the Herbrand Universe) and predicate con- classroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributed structors(generatingtheHerbrandBase). forprofitorcommercialadvantageandthatcopiesbearthisnoticeandthefullcitation Recursive data types in programming languages like Haskell, onthefirstpage.Tocopyotherwise,torepublish,topostonserversortoredistribute tolists,requirespriorspecificpermissionand/orafee. ML,Scalacanbeseenasanotationforfreealgebras.Wereferto [19]foraclearandconvincingdescriptionofthisconnection. Copyright(cid:13)c ACM...$10.00 Forinstance,theHaskelldeclarations data AlgU = U | S AlgU Note that this property corresponds of the initial algebra [19] data AlgB = B | O AlgB | I AlgB viewofthecorresponding(ordered,rooted)binarytreedatatype. data AlgT = T | C AlgT AlgT DEFINITION5. If u : X → Y, we denote M(u) : M(X) → correspond,respectivelyto M(Y)theuniquemorphismofmagmasdefinedbytheconstruction • the free algebra AlgU with a single generator U and unary inProposition1. constructorS(thatcanbeseenaspartofthelanguageofPeano Ifv : Y → Z thenthemorphismM(v)◦M(u)extendsv◦u : orRobinsonarithmetic,orthedecidable(W)S1Ssystem,[2]) X →ZandthereforeM(v)◦M(u)=M(v◦u). • the free algebra AlgB with single generator B and two unary constructors O and I (corresponding to the language of the PROPOSITION2. Ifu : X → Y isrespectivelyinjective,surjec- decidable system (W)S2S [11]), as well as “bijective base-2” tive,bijectivethensoisM(u). numbernotation[20] Itfollowsthat • the free algebra AlgT with single generator T and one binary constructor C (essentially the same thing as the free magma PROPOSITION3. IfX = {x}andY = {y}andu : X → Y is generatedbyT). thebijectionsuchthatf(x) = y,thenM(u) : M(X) → M(Y) isabijectivemorphism(i.e.anisomorphism)offreemagmas. Theset-theoreticalconstructioncorrespondingtothe“|”operation isdisjointunionandthedatatypescorrespondtoinfinitesetsgen- Proof IfX isemptysoisM(X),henceuisinjective.Ifuisin- eratedbyapplyingtherespectiveconstructorsrepeatedly.Theset- jective, then ∃u(cid:48) : Y → X,u(cid:48) ◦u = id where id M(X) M(X) theoreticalinterpretationof“self-reference”insuchdatatypedefi- denotestheidentitymappingofM(X).ThenM(u(cid:48))◦M(u) = nitionscanbeseenasfixpointoperationonsetsofnaturalnumbers M(u(cid:48)◦u)=id andhenceM(u)isinjective.Ifuissurjec- M(X) asshowninthePωconstructionusedbyDanaScottindefiningthe tive,then∃u(cid:48) :Y →X,u◦u(cid:48) =id .ThenM(u)◦M(u(cid:48))= M(Y) denotationalsemanticsforvariousλ-calculusconstructs[13]. M(u◦u(cid:48))=id andhenceM(u)issurjective.Ifuisbijec- M(Y) Wewillnext“instantiate”somegeneralresultstomaketheun- tive,thanitisinjectiveandsurjectiveandsoisM(u). derlyingmathematicsaselementaryandself-containedaspossible. Whilecategorytheoryisfrequentlyusedasthemathematicalback- WewillidentifythedatatypeAlgTwiththefreemagmagener- ingfordata-types,wewillprovidehereasimplesettheory-based atedbytheset{T}anddenoteitsbinaryoperationx∗yasC x y. formalism,alongthelinesof[1]. Itcorrespondstothefreealgebra(thatwewillalsodenoteAlgT) WewillstartwiththeelementarymathematicsbehindtheAlgT definedbythesignature{T/0, C/2}. datatypeandfollowwithanoutlineforasimilartreatmentofAlgU We can now instantiate the results described by the previous andAlgB. propositionstoAlgT: 2.1 Thefreemagmaoforderedrootedbinarytreeswith PROPOSITION4. LetXbeanalgebradefinedbyaconstanttand emptyleaves abinaryoperationc.Thenthere’sauniquemorphismf : AlgT → Xthatverifies DEFINITION2. AsetM witha(total)binaryoperation∗iscalled amagma. f(T)=t (1) DEFINITION3. AmorphismbetweentwomagmasM andM(cid:48)isa f(C(x,y))=c(f(x),f(y)) (2) functionf :M →M(cid:48)suchthatf(x∗y)=f(x)∗f(y). Moreover,ifXisafreealgebrathenf isanisomorphism. Let X be a set. We define the sets Mn(X) inductively as Proof ItfollowsfromProposition2andequationf(T)=t,given follows:M1(X)=Xandforn>1,Mn(X)isthedisjointunion thatf isabijectionbetweenthesingletonsets{T}and{t}. ofthesetsM (X)×M (X)for0 < k < n.LetM(X)be k n−k the disjoint union of the family of sets M (X) for n > 0. We 2.2 TheOneSuccessorandTwoSuccessorsFreeAlgebras n identifyeachsetM withitscanonicalimageinM(X).Thenfor n Theonesuccessorfreealgebra(alsoknownasunarynaturalnum- w ∈ Mn(X), we call n the length of w and denote it l(w). Let bersorPeanoalgebra,aswellasthelanguageofthemonoid{0}∗ w,w(cid:48) ∈ M(X)andletp = l(w)andq = l(w(cid:48)).Theimageof and the decidable systems WS1S and S1S) is defined by the sig- (w,w(cid:48)) ∈ M ×M under the canonical injection in M(X) is p q nature{U/0, S/1},whereUisaconstant(seenaszero)andSis calledthecompositionofwandw(cid:48)andisdenotedw∗w(cid:48). theunarysuccessorfunction.WewilldenoteAlgUthisalgebraand When X = {T} where T is interpreted as the “empty” leaf identifyitwithitscorrespondingdatatype. oforderedrootedbinarytrees,theelementsofM canbeseenas n WestateananalogueofProposition4forthefreealgebraAlgU. ordered rooted binary trees with n leaves while the composition operation“∗”representsjoiningtwotreesattheirrootstoforma PROPOSITION5. LetXbeanalgebradefinedbyaconstantuand newtree. aunaryoperations.Thenthere’sauniquemorphismf : AlgU → Xthatverifies DEFINITION4. The set M(X) with the composition operation (w,w(cid:48))→w∗w(cid:48)iscalledthefreemagmageneratedbyX. f(U)=u (3) f(S(x))=s(f(x)) (4) PROPOSITION1. Let M be a magma. Then every mapping u : X →McanbeextendedinauniquewaytoamorphismofM(X) Moreover,ifXisafreealgebrathenf isanisomorphism. intoM. Notethatfollowingtheusualidentificationofdatatypesandinitial Proof We define inductively the mappings f : M (X) → M algebras, AlgU corresponds to the initial algebra “1 + ” through n m as follows: For n = 1,f = f. For n > 1,∀p ∈ {1,..,n − theoperationg=<U,S>seenasabijectiong:1+N→N. 1 1},f (w∗w(cid:48)) = f (w)∗f (w(cid:48)).Letg : M(X) → M such Thetwosuccessorfreealgebra(alsoknownasbijectivebase- n p n−p that∀n > 0,∀x ∈ M (X),g(x) = f (x).Thengistheunique 2 natural numbers or Peano algebra, as well as the language of n n morphismofM(X)intoMwhichextendsf. themonoid{0,1}∗ andthedecidablesystemsWS2SandS2S)is definedbythesignature{B/0, O/1, I/1} whereBisaconstant case C(T, T) ⇒ T (seen as the empty sequence) and O, I are two unary successor case C(T, y) ⇒ d(y) functions.WewilldenoteAlgBthisalgebraandidentifyitwithits case z ⇒ C(T, p(h(z))) correspondingdatatype. } WecanstateananalogueofProposition4forthefreealgebra Notethepredecessorfunctioncalledpandourauxiliaryfunctions AlgB. namedd(which“doubles”itsinput,assumeddifferentfromT)and PROPOSITION6. Let X be an algebra defined by a constant b h(which“halves”itsinput,assumed“even”anddifferentfromT). andatwounaryoperationso,i.Thenthere’sauniquemorphism def d(z: AlgT): AlgT = z match { f : AlgB →Xthatverifies case C(x, y) ⇒ C(s(x), y) f(B)=b (5) } f(O(x))=o(f(x)) (6) def h(z: AlgT): AlgT = z match { case C(x, y) ⇒ C(p(x), y) f(I(x))=i(f(x)) (7) } Moreover,ifXisafreealgebrathenf isanisomorphism. } We will define our generalized constructor/destructor S rep- Theseobservationssuggestthatfordefiningisomorphismsbe- resenting the successor function and predecessor function on tweenAlgU, AlgBandAlgTthatenableacompletesetofequiva- rootedorderedbinarytreesoftypeAlgTbyprovidingapplyand lentarithmetic(andlaterset-theoretic)operationsoneachofthem, unapplymethodsexpressedintermsofour“real”constructorsT wewillneedamechanismtoprovesuchequivalences.Tothisend, andCandtheactualalgorithmsdefinedinthe(shared)traitAlgT. itwillbeenoughtoprovethatsuchnon-constructoroperationsalso formfreealgebrasofmatchingsignatures. object S extends AlgT { Wewillcalltermstheelementsofourinitialalgebras. def apply(x: AlgT) = s(x) 3. GeneralizedConstructors def unapply(x: AlgT) = x match { case C(_, _) ⇒ Some(p(x)) The iso-functors supporting the equivalence between actual con- case T ⇒ None structors and their recursively defined function counterparts sug- } gestexploringprogramminglanguageconstructsthattreatthemin } asimilarway.Forinstanceitmakessensetoextend“constructor- The definition of the generalized constructor/destructor D repre- onlybenefits”likepatternmatchingtotheirfunctioncounterparts. sentingdouble/halfissimilar.Notetheuseofthemethodddefined Fortunately, constructors/deconstructors generalized to arbi- inthetraitAlgT. trary functions are available in Scala through apply/unapply methods and in Haskell through a special notation implement- object D extends AlgT { ing views, under the implicit assumption that they define inverse def apply(x: AlgT) = d(x) operations. Onecanimmediatelynoticethatourfreealgebrasprovidesuf- def unapply(x: AlgT) = x match { ficient conditions under which this assumption is enforced. This case C(C(_, _), _) ⇒ Some(h(x)) suggests the possibility that such generalized constructor/decon- case _ ⇒ None } structorpairscouldprovidethecombinedbenefitsofpatternmatch- } inganddataabstraction,withtheimplicationthatdirectsyntactic supportforsuchconstructscanbringsignificantexpressivenessto The definition of the generalized constructor/destructor O can be functionalprogramminglanguages. seenascorrespondingtoλx.2x+1anditsinverse. 3.1 GeneralizedConstructorswithapply/unapplyinScala object O extends AlgT { def apply(x: AlgT) = C(T, x) Besides supporting case classes and case objects that are used(amongotherthings)toimplementpatternmatching,Scala’s def unapply(x: AlgT) = x match { apply and unapply methods [5, 10] allow definition of cus- case C(T, b) ⇒ Some(b) tomizedconstructorsanddestructors(calledextractorsinScala). case _ ⇒ None WewillnextdescribehowarithmeticoperationswithourAlgT } terms,representedasorderedrootedbinarytrees,canbenefitfrom } theusesuch“generalizedconstructors”. The definition of the generalized constructor/destructor O can be Our AlgT free algebra will correspond in Scala to a case seenascorrespondingtoλx.2x+2anditsinverse.Notetheuse object / case class definition, combined with a mechanism of the generalized constructors S, D and O, both on the left and toshareactualcode,encapsulatedintheAlgTtrait. right side of match statements, illustrating their usefulness both case object T extends AlgT asconstructorsandasextractors. case class C(l: AlgT, r: AlgT) extends AlgT object I extends AlgT { trait AlgT { def apply(x: AlgT) = S(O(x)) def s(z: AlgT): AlgT = z match { case T ⇒ C(T, T) def unapply(x: AlgT) = x match { case C(T, y) ⇒ d(s(y)) case D(a) ⇒ Some(p(a)) case z ⇒ C(T, h(z)) case _ ⇒ None } } } def p(z: AlgT): AlgT = z match { 3.2 AScala-basedNaturalNumberArithmeticPackage } usingAlgTTerms } Wewillnowillustratehowtheuseofgeneralizedconstructorshelps Similarly, a constant time complexity definition is given here for writing a fairly complete set of arithmetic algorithms on therms theexponentof2operation,byusingthe“real”constructorC. of AlgT seen as natural numbers. For comparison purposes, the def exp2(x: AlgT) = C(x, T) readermightwanttolookattheHaskellcodein[17]wheresimi- laralgorithmsareexpressedusingatypeclass-basedmechanism. Thepoweroperationpowtakesadvantageofthegeneralizedcon- However,whiletheuseoftypeclassescomeswiththebenefitsof structorsOandIontheleftsideofacasestatementthroughthe data abstraction it needs separate functions for constructing, de- AlgBviewofAlgT. constructingandrecognizingtermstoexpresstheequivalentofthe generalizedconstructorsusedhere. def pow(u: AlgT, v: AlgT): AlgT = (u, v) match { case (_, T) ⇒ C(T, T) WestartwithacomparisonfunctionreturningLT, EQ, GTand case (x, O(y)) ⇒ multiply(x, pow(multiply(x, x), y)) supportingatotal orderrelationonAlgT,isomorphictotheone case (x, I(y)) ⇒ { on N. Note here the use of the generalized constructors O and I val xx = multiply(x, x) providingaviewofthetermsofAlgTastermsofthefreealgebra multiply(xx, pow(xx, y)) BinT. } } trait Tcompute extends AlgT { def cmp(u: AlgT, v: AlgT): Int = (u, v) match { Efficientdivisionwithremainderisaslightlymorecomplexalgo- case (T, T) ⇒ EQ rithm,wherewetakeadvantageofgeneralizedconstructors,direct case (T, _) ⇒ LT inheritancefromtraitAlgTaswellasnumberofpreviouslydefined case (_, T) ⇒ GT functions: case (O(x), O(y)) ⇒ cmp(x, y) case (I(x), I(y)) ⇒ cmp(x, y) def div_and_rem(x: AlgT, y: AlgT): (AlgT, AlgT) = case (O(x), I(y)) ⇒ strengthen(cmp(x, y), LT) if (cmp(x, y) == LT) (T, x) case (I(x), O(y)) ⇒ strengthen(cmp(x, y), GT) else if (T == y) null // division by zero } else { def try_to_double(x:AlgT, y:AlgT, k:AlgT): AlgT = val LT = -1 if (cmp(x, y) == LT) p(k) val EQ = 0 else try_to_double(x, D(y), S(k)) val GT = 1 def divstep(n: AlgT, m: AlgT): (AlgT, AlgT) = { private def strengthen(rel: Int, from: Int) = val q = try_to_double(n, m, T) rel match { val p = multiply(exp2(q), m) case EQ ⇒ from (q, sub(n, p)) case _ ⇒ rel } } val (qt, rm) = divstep(x, y) val (z, r) = div_and_rem(rm, y) Additionisexpressedcompactlyintermsofthegeneralizedcon- val dv = add(exp2(qt), z) structorsO,IandS. (dv, r) } def add(u: AlgT, v: AlgT): AlgT = (u, v) match { case (T, y) ⇒ y Division and reminder can be separated using Scala’s projection case (x, T) ⇒ x functions: case (O(x), O(y)) ⇒ I(add(x, y)) case (O(x), I(y)) ⇒ O(S(add(x, y))) def divide(x: AlgT, y: AlgT) = div_and_rem(x, y)._1 case (I(x), O(y)) ⇒ O(S(add(x, y))) case (I(x), I(y)) ⇒ I(S(add(x, y))) def reminder(x: AlgT, y: AlgT) = div_and_rem(x, y)._2 } Finally, the greatest common divisor gcd and the least common Thedefinitionofsubtractionissimilar,exceptthatthecodeofthe multiplierlcmaredefinedasfollows: predecessorfunctionpisconvenientlyinheriteddirectlyfromthe def gcd(x: AlgT, y: AlgT): AlgT = traitAlgT,giventhatthetraitTcomputeextendsit. if (y == T) x else gcd(y, reminder(x, y)) def sub(u: AlgT, v: AlgT): AlgT = (u, v) match { case (x, T) ⇒ x def lcm(x: AlgT, y: AlgT): AlgT = case (O(x), O(y)) ⇒ p(O(sub(x, y))) multiply(divide(x, gcd(x, y)), y) case (O(x), I(y)) ⇒ p(p(O(sub(x, y)))) } case (I(x), O(y)) ⇒ O(sub(x, y)) The trait Tconvert implements efficiently conversion to/from case (I(x), I(y)) ⇒ p(O(sub(x, y))) Scala’s BigInt arbitrary size integers using bit-level operations } correspondingtopowerof2andrecognitionofoddandevennatu- ThemultiplicationoperationissimilartotheHaskellcodeinsec- ralnumbers.ThefunctionfromNbuildsanAlgTtreerepresentation tion??,exceptfortheuseofthegeneralizedconstructorO. equivalenttoaBigInt. def multiply(u: AlgT, v: AlgT): AlgT = (u, v) match { trait Tconvert { case (T, _) ⇒ T def fromN(i: BigInt): AlgT = { case (_, T) ⇒ T def oddN(i: BigInt) = case (C(hx, tx), C(hy, ty)) ⇒ { i.testBit(0) val v = add(tx, ty) val z = p(O(multiply(tx, ty))) def evenN(i: BigInt) = C(add(hx, hy), add(v, z)) i != BigInt(0) && !i.testBit(0) The actual code will be shared through the trait Qcode that also def hN(x: BigInt): BigInt = mixes-infunctionalityfromthenaturalnumberoperationsdefined if (oddN(x)) inthetraitsTcomputeandTconvert. BigInt(0) Westartwithatypedefinitionfororderedpairsofnaturalnum- else bersPQrepresentedastermsofAlgTandtheconversionfunction BigInt(1) + hN(x >> 1) toaconventionalfractionrepresentedasanorderedpairofBigInt objects.TheconversionfunctiontoFraqusestheAlgTtoBigInt def tN(x: BigInt): BigInt = if (oddN(x)) convertertoN. (x - BigInt(1)) >> 1 trait Qcode extends Tcompute with Tconvert { else type PQ = (AlgT, AlgT) tN(x >> 1) def toFraq(): (BigInt, BigInt) = this match { if (0 == i) T case Z ⇒ (0, 1) else C(fromN(hN(i)), fromN(tN(i))) case M((a, b)) ⇒ (-(toN(a)), toN(b)) } case P((a, b)) ⇒ (toN(a), toN(b)) ThefunctiontoNconvertsanAlgTtreerepresentationtoaBigInt. } def toN(z: AlgT): BigInt = z match { Thefunctiont2pqsplitsitsargumentuseenasanaturalnumber case T ⇒ 0 intoitscorrespondingCalkin-Wilfrational,representedasapairof case C(x, y) ⇒ positivenaturalnumbersoftypePQ.Notetheuseofourgeneralized (BigInt(1) << toN(x).intValue()) ∗ constructorsOandIdistinguishingbetweenoddandevennumbers. (BigInt(2) ∗ toN(y) + 1) ThealgorithmusesanencodingofthepathintheCalkin-Wilftree } asamemberofAlgB,whereOisinterpretedasacommandtotake } theleftbranchandIisinterpretedasacommandtotaketheright Notethatforboththeseconversionswehaveused,forefficiency branchatanodeoftheCalkin-Wilftree(showninFig.1,forafew reasons, the “real constructors” T and C, although much simpler smallpositiverationals,representedasconventionalfractions). (andslower)converterscanbebuiltusingeithertheAlgBorAlgU viewofAlgTterms. TheuseofScala’sgeneralizedconstructorsinspiredbyourfree algebra isomorphisms has shown the combined flexibility of in- heritanceasamechanismfordataabstractionandconvenientpat- ternmatchingallowingthedesignofouralgorithmsinafunctional style.Theimplicituseofapplyandunapplymethodsincombina- tionwithoursimplefreealgebrasemanticshasfacilitatedthesafe useoffairlycomplex(mutually)recursivefunctionsinthedefini- tion of the generalized constructors. The use of Scala’s traits has facilitatedflexibleinheritancemechanismssupportingshareddefi- nitionswithoutanyadditionalsyntacticclutter. Figure1. TheCalkin-WilfTree 4. AnApplication:RationalArithmeticinScala def t2pq(u: AlgT): PQ = u match { withCalkin-WilfTrees case T ⇒ (S(T), S(T)) We will extend our Scala code snippet described in subsection case O(n) ⇒ { val (x, y) = t2pq(n) 3.1toarealisticarbitrarysizearithmeticpackage.Itissomewhat (x, add(x, y)) unconventional, as it is based on the Calkin-Wilf bijection [3, 6] } betweenNandthesetofpositiverationalnumbersQ+,ratherthan case I(n) ⇒ { moretypicalrepresentationslikethearraysoflongwordsusedin val (x, y) = t2pq(n) Java’sBigDecimalpackage,alsoadoptedthroughawrapperclass (add(x, y), y) withthesamenamebyScala(whichrunsontopoftheJavaVirtual } Machine). } Amongitsadvantages,division(withnon-zero)alwaysreturnsa Thefunctionpq2tfusesbackintoa“naturalnumber”represented finitelyrepresentedrationaland“nobitislost”intherepresentation asatermofAlgT,correspondingtothepathintheCalkin-Wilftree, ascanonicalrationalnumberswithco-primenumerator/denomina- apairofco-primenaturalnumbersrepresentingthe(numerator, torpairsarebijectivelymappedtonaturalnumbers.Ourapproach denominator)pairdefiningapositiverationalnumber. emphasizesthefactthatamathematicalconceptdefinedtradition- ally through equivalence classes and quotients, can be expressed def pq2t(uv: PQ): AlgT = uv match { entirelyintermsofafreealgebra-basedmechanism. case (O(T), O(T)) ⇒ T ThetraitQrepresentingourrationalnumberdatatypecontains case (a, b) ⇒ distinctconstructorsforpositive(P),negativenumbers(M)andzero cmp(a, b) match { (Z). case GT ⇒ I(pq2t(sub(a, b), b)) case LT ⇒ O(pq2t(a, sub(b, a))) trait Q extends Qcode } } case object Z extends Q Thisbringsustothedefinitionofthebijectionbetweensignedra- case class P(x: (AlgT, AlgT)) extends Q case class M(x: (AlgT, AlgT)) extends Q tionalsandtermsseenthroughtheuseofourgeneralizedconstruc- torsOandIastermsofAlgBrepresentingnaturalnumbers. def fromT(t: AlgT): Q = t match { val (u, v) = uv case T ⇒ Z // zero → zero cmp(multiply(x, v), multiply(y, u)) case O(x) ⇒ M(t2pq(x)) // odd → negative } case I(x) ⇒ P(t2pq(x)) // even → positive } Multiplication,inverseanddivisiononQ+aredefinedasusual. ItsinversefromsignedrationalstotermsofAlgT,seenasnatural def pqmultiply(a: PQ, b: PQ) = numbers,proceedsbycaseanalysisontheQdatatype.Notethat pqsimpl(multiply(a._1, b._1), multiply(a._2, b._2)) positivesignisencodedbymappingtoevennaturalsandnegative signisencodedbymappingtooddnaturals. def pqinverse(a: PQ) = (a._2, a._1) def toT(q: Q): AlgT = q match { def pqdivide(a: PQ, b: PQ) = pqmultiply(a, pqinverse(b)) case Z ⇒ T // zero → zero case M(x) ⇒ O(pq2t(x)) // negative → odd Wearereadytodefinearithmeticoperationsonthesetofsigned case P(x) ⇒ I(pq2t(x)) // positive → even rationalsQ,bycaseanalysisontheirsign.Westartwiththeoppo- } siteofarational. The bijection between Scala’s BigInt, seen as a natural num- def ropposite(x: Q) = x match { ber type and signed rationals, is defined as the pair of functions case Z ⇒ Z rat2natandnat2rat case M(a) ⇒ P(a) case P(a) ⇒ M(a) def nat2rat(n: BigInt): Q = fromT(fromN(n)) } def rat2nat(q: Q): BigInt = toN(toT(q)) Addition is defined by case analysis on the sign and calls to the Next we define a simplifier of positive fractions represented as a appropriateoperationsonpositiverationals. pair,tofacilitatearithmeticoperationsonourrationals. def radd(a: Q, b: Q): Q = (a, b) match { def pqsimpl(xy: PQ) = { case (Z, y) ⇒ y val x = xy._1 case (M(x), M(y)) ⇒ M(pqadd(x, y)) val y = xy._2 case (P(x), P(y)) ⇒ P(pqadd(x, y)) val z = gcd(x, y) case (P(x), M(y)) ⇒ pqcmp(x, y) match { (divide(x, z), divide(y, z)) case LT ⇒ M(pqsub(y, x)) } case EQ ⇒ Z case GT ⇒ P(pqsub(x, y)) We also use our simplifier to import and export non-canonically } representedrationalsrepresentedasBigIntpairs. case (M(x), P(y)) ⇒ ropposite(radd(P(x), M(y))) def fraq2pq(nd: (BigInt, BigInt)): PQ = } pqsimpl((fromN(nd._1), fromN(nd._2))) Subtractionisdefinedsimilarly. def pq2fraq(nd: PQ): (BigInt, BigInt) = def rsub(a: Q, b: Q) = radd(a, ropposite(b)) (toN(nd._1), toN(nd._2)) def rmultiply(a: Q, b: Q): Q = (a, b) match { Wearenowreadyforourarithmeticoperations.Thetemplatefunc- case (Z, _) ⇒ Z tionpqop,parameterizedbyafunctionf,willbesharedbetween case (_, Z) ⇒ Z additionandsubtraction.Notethatitalsoinvolvessimplification, case (M(x), M(y)) ⇒ P(pqmultiply(x, y)) toensurethattheresultsareinacanonicalco-primenumerator/de- case (M(x), P(y)) ⇒ M(pqmultiply(x, y)) nominatorform. case (P(x), M(y)) ⇒ M(pqmultiply(x, y)) case (P(x), P(y)) ⇒ P(pqmultiply(x, y)) def pqop(f: (AlgT, AlgT) ⇒ AlgT, xy:PQ, uv:PQ):PQ = { } val (x, y) = xy val (u, v) = uv Finallywedefinetheinverseonnon-zerorationals val z = gcd(y, v) val y1 = divide(y, z) def rinverse(a: Q) = a match { val v1 = divide(v, z) case M(x) ⇒ M(pqinverse(x)) val num = f(multiply(x, v1), multiply(u, y1)) case P(x) ⇒ P(pqinverse(x)) val den = multiply(z, multiply(y1, v1)) } pqsimpl((num, den)) } anduseittoderivefromitadivisionoperationonQ Wecanuseittodefineadditionandsubtractionofpositiverationals def rdivide(a: Q, b: Q) = by simply instantiating our function parameter f to add and sub rmultiply(a, rinverse(b)) operatingontermsofAlgT. } def pqadd(a: PQ, b: PQ) = pqop(add, a, b) These operations conclude the trait Qcode. While this complete arithmeticpackagewasbuiltmostlyasaproofofconceptforthe def pqsub(a: PQ, b: PQ) = pqop(sub, a, b) expressivenessofourfreealgebrabasedapproachonprogressively moreinterestingmathematicalobjects,futureworkisplannedfor ThecomparisonoperationprovidingatotalorderingofQ+ relies turningthispackageintoapracticaltool.Afirstobservationtoward on the function cmp comparing terms of AlgT seen as natural this end is that, like in the case of Java’s BigIntegers or the C- numbers. based GMP package, one needs to use a hybrid approach, taking def pqcmp(xy: PQ, uv: PQ) = { advantageofactualmachinewords(64bitsatthispoint),tostore val (x, y) = xy andoperateonnumbersthatfitinamachineword. 5. RelatedWork [4] T.CoquandandG.Huet. Thecalculusofconstructions. Information andComputation,76(2/3):95–120,1988. Numeration systems on regular languages have been studied re- cently,e.g.in[12]andspecificinstancesofthemarealsoknownas [5] BurakEmir,MartinOdersky,andJohnWilliams. Matchingobjects withpatterns. InErikErnst,editor,ECOOP2007-Object-Oriented bijectivebase-knumbers[20].ArithmeticpackagessimilartoAlgU Programming,volume4609ofLectureNotesinComputerScience, andAlgBarepartoflibrariesofproofassistantslikeCoq[9]and pages273–298.SpringerBerlin/Heidelberg,2007. thecorrespondingregularlanguageshavebeenusedasabasisof [6] Jeremy Gibbons, David Lester, and Richard Bird. Enumer- decidablearithmeticsystemslike(W)S1S[2]and(W)S2S[11]. ating the rationals. Journal of Functional Programming, 16 Arithmeticcomputationsbasedonmorecomplexrecursivedata (4), 2006. URL http://www.comlab.ox.ac.uk/oucl/work/ types like the free magma of binary trees (essentially isomorphic jeremy.gibbons/publications/rationals.pdf. tothecontext-freelanguageofbalancedparentheses)aredescribed [7] K.Go¨del.U¨bereinebishernochnichtbenu¨tzteErweiterungdesfiniten in[17]and[16],wheretheyareseenasGo¨del’sSystem Ttypes, Standpunktes.Dialectica,12(280-287):12,1958. aswellascombinatorapplicationtrees.In[15]atypeclassmecha- [8] NaokiKobayashi,KazutakaMatsuda,andAyumiShinohara. Func- nismisusedtoexpresscomputationsonhereditarilyfinitesetsand tionalProgramsasCompressedData. ACMSIGPLAN2012Work- hereditarily finite functions. However, none of these papers pro- shoponPartialEvaluationandProgramManipulation,January2012. vides proofs of the properties of the underlying free algebras or ACMPress. usesmechanismssimilartothegeneralizedconstructorsdescribed [9] TheCoqdevelopmentteam. TheCoqproofassistantreferenceman- inthispaper. ual. LogiCalProject,2004. URLhttp://coq.inria.fr. Version A very nice functional pearl [6] has explored in the past (us- 8.0. ing Haskell code) algorithms related to the Calkin-Wilf bijection [10] M.Odersky,L.Spoon,andB.Venners.ProgramminginScala.Artima [3].Whileusingthesameunderlyingmathematics,ourScala-based Inc,2008. packageworksontermsoftheAlgTfreealgebraratherthancon- [11] Michael. O. Rabin. Decidability of second-order theories and au- ventional numbers, and provides a complete package of arbitrary tomataoninfinitetrees. TransactionsoftheAmericanMathematical sizerationalarithmeticoperationstakingadvantageofourgeneral- Society,141:1–35,1969. izedconstructors. [12] MichelRigo. Numerationsystemsonaregularlanguage:arithmetic operations,recognizabilityandformalpowerseries.TheoreticalCom- 6. Conclusion puterScience,269(12):469–498,2001.ISSN0304-3975. [13] DanaScott. DataTypesasLattices. SiamJ.Comput.,5(3):522–587, We have shown that free algebras corresponding to some basic 1976. data types in programming languages can be used for arithmetic computationsisomorphictotheusualoperationsonN. [14] PaulTarau.“EverythingIsEverything”Revisited:ShapeshiftingData TypeswithIsomorphismsandHylomorphisms. ComplexSystems, Asanewtheoreticalcontribution,wehaveworked-outdetailsof (18):475–493,2010. proofs,basedonlyonelementarymathematics,ofessentialproper- tiesofthemutuallyrecursivesuccessorandpredecessorfunctions, [15] PaulTarau.Declarativemodelingoffinitemathematics.InPPDP’10: Proceedingsofthe12thinternationalACMSIGPLANsymposiumon onthefreealgebraAlgToforderedrootedbinarytrees. Principlesandpracticeofdeclarativeprogramming,pages131–142, Aconceptofgeneralizedconstructor,forwhichwehavefound NewYork,NY,USA,2010.ACM. simpleimplementationsinScala,hasbeenintroduced.Bywork- [16] PaulTarau. DeclarativeSpecificationofTree-basedSymbolicArith- ing in synergy with our free algebra isomorphisms we have de- meticComputations. InClaudioRussoandNeng-FaZhou,editors, scribed,usinglanguageconstructslikeScala’sapply / unapply, Proceedings of PADL’2012, Practical Aspects of Declarative Lan- simple and safe means to combine data abstraction and pattern guages, pages 273–289, Philadelphia, PA, January 2012. Springer, matchinginmodern-dayfunctionalandobjectorientedlanguages. LNCS7149. Asanewpracticalcontribution,acompletearbitrarysizesigned [17] Paul Tarau and David Haraburda. On Computing with Types. In rationalnumberpackagewritteninScalahasbeenderivedworking ProceedingsofSAC’12,ACMSymposiumonAppliedComputing,PL withtermsoftheAlgTfreealgebraofrootedorderedbinarytrees track,pages1889–1896,RivadelGarda(Trento),Italy,March2012. withemptyleaves. [18] DimitriosVytiniotisandAndrewKennedy. FunctionalPearl:Every Futureworkisplannedtoinvestigatepossiblepracticalapplica- Bit Counts. ICFP 2010 : The 15th ACM SIGPLAN International tionsofouralgorithmstosymbolicand/orarbitrarylengthinteger Conference on Functional Programming, September 2010. ACM arithmeticpackagesandtoparallelexecutionofarithmeticcompu- Press. tationsonAlgT. [19] Philip Wadler. Recursive Types for Free! 1990. unpub- ThecodesnippetshowingtheuseofScala’sapplyandunapply lishedmanuscriptathttp://homepages.inf.ed.ac.uk/wadler/ methods to support generalized constructors as well as the arith- papers/free-rectypes/free-rectypes.txt. meticonrationalsisavailableasaseparatefileathttp://######. [20] Wikipedia. Bijectivenumeration—wikipedia,thefreeencyclopedia, 2012. URL http://en.wikipedia.org/w/index.php?title= Bijective_numeration&oldid=483462536.[Online;accessed2- Acknowledgement June-2012]. ThisresearchhasbeensupportedbyNSFgrant######. References [1] Nicolas Bourbaki. Elements of Mathematics, Algebra I. Springer, BerlinHeidelbergNewYork,1989. [2] J.R.Bu¨chi. Onadecisionmethodinrestrictedsecondorderarith- metic. InternationalCongressonLogic,Method,andPhilosophyof Science,141:1–12,1962. [3] N.CalkinandH.S.Wilf. RecountingtheRationals. AmericanMath Monthly,,107:360–363,2000.