úΨŠ¢ìQ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOP%Basic lambda term size model notions.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe Lambda term size model. Size of zeroSize of successorSize of the abstractionSize of the applicationaChecks whether the given size model is valid in the framework of Gittenberger and GoBbiewski.The natural size notion.The binary size notion. öGiven a size notion, returns a tuple (a,b,c,d) where a denotes the size of the de Bruijn zero, b denotes the size of the de Bruijn successor, c denotes the size of the lambda abstraction and finally d denotes the size of the application.  Size notion Whether the size model is valid.Q   Q 'Lambda terms in the de Bruijn notation.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe $Lambda terms with de Bruijn indices. de Bruijn indices. Lambda abstraction. Term application.$de Bruijn indices in unary notation.?Translates the given index to a corresponding positive integer.?Translates the given positive integer to a corresponding index.'Predicate defining closed lambda terms.1Finds the maximal index in the given lambda term.+Computes the size of the given lambda term./Computes the size of the given de Bruijn index. %Size notion used in the computations.The considered lambda term.$The integer size of the lambda term.%Size notion used in the computations.The considered de Bruijn index.$The integer size of the lambda term.    Basic Boltzmann oracle notions.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe RlFunction f whose real root constitutes the singularity for plain lambda terms in the given size model.SThe derivative of domFunc.TyFunction f_h whose real root constitutes the singularity for closed h-shallow lambda terms in the given size model.UThe derivative of domFuncH.V&Newton-Raphson root finding algorithm.SSuccessive root approximations of the plain lambda terms dominating singularity.^Successive root approximations of the closed h-shallow lambda terms dominating singularity.XFinds the dominating singularity of the plain lambda term ordinary generating function.cFinds the dominating singularity of the closed h-shallow lambda term ordinary generating function. WR Size notion.Formal z parameter.The value f(z).ST Size notion. Shallowness.Formal z parameter.The value f_h(z).UV%Function f whose root is to be found.The derivative f'.Initial guess. Infinite approximation sequence. Size notion.Initial guess. Infinite approximation sequence. Size notion. Shallowness.Initial guess. Infinite approximation sequence.X Size notion.Approximation error.Dominating singularity. Size notion. Shallowness.Approximation error.Dominating singularity. WRSTUVX`Basic notions regarding combinatorial specifications defining plain lambda terms.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe kBoltzmann sampler specification consisting of a Boltzmann system with a corresponding size notion model.Boltzmann system.  Size notion.!dAn expression defining the branching probabilities in the Boltzmann model for plain lambda terms.#Abstraction probability.$Application probability.%Zero constructor probability.&nEvaluates the generating function for plain lambda terms assuming the given size model and parameter value.'XComputes the Boltzmann model for plain lambda terms evaluated in the given parameter.(hComputes the Boltzmann sampler specification for plain lambda terms evaluated in the given parameter.)mComputes the rejection Boltzmann sampler for plain lambda terms evaluated near the dominating singularity. !"#$%&Y' Size notion.Formal z parameter.The computed Boltzmann system.( Size notion.Formal z parameter.The computed Boltzmann sampler.) Size notion. Singularity approximation error.)The computed rejection Boltzmann sampler.  !"$#%&'() !"#$%' ()& !"#$%&Y'()dBasic notions regarding combinatorial systems defining closed h-shallow lambda terms.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe +kBoltzmann sampler specification consisting of a Boltzmann system with a corresponding size notion model.-Boltzmann system.. Size notion./HCombinatorial system specification for closed h-shallow lambda terms.0oAn expression defining the branching probabilities in the Boltzmann model for closed h-shallow lambda terms.2Abstraction probability.3Application probability.4#Probabilities for de Bruijn indices5cComputes the Boltzmann model for closed h-shallow lambda terms evaluated in the given parameter.6_Computes the mixed Boltzmann model for closed lambda terms evaluated in the given parameter.7sComputes the Boltzmann sampler specification for closed h-shallow lambda terms evaluated in the given parameter.8xComputes the rejection Boltzmann sampler for closed h-shallow lambda terms evaluated near the dominating singularity.+,-./01234Z[\]^5 Size notion. Shallowness.Formal z parameter.The computed Boltzmann system.6 Size notion. Shallowness.Formal z parameter.The computed Boltzmann system._`a7 Size notion. Shallowness.Formal z parameter.The computed Boltzmann sampler.8 Size notion. Shallowness. Singularity approximation error.)The computed rejection Boltzmann sampler.+,-./01324567801234/56+,-.78+,-./01234Z[\]^56_`a78SBasic notions regarding combinatorial systems defining lambda terms.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe:kBoltzmann sampler specification consisting of a Boltzmann system with a corresponding size notion model.<Boltzmann system.= Size notion.>ÿAn expression defining the branching probabilities in the Boltzmann model for unbounded closed lambda terms using a mixture of a system for closed shallow terms and a closure system for plain terms used once the closed system has been exceeded in the sampling procedure.B‘Computes the Boltzmann model for closed lambda terms evaluated in the given parameter using closed h-shallow terms as a base approximation.CiComputes the Boltzmann sampler specification for closed lambda terms evaluated in the given parameter.DnComputes the rejection Boltzmann sampler for closed lambda terms evaluated near the dominating singularity. :;<=>?@AB Size notion. Shallowness.Formal z parameter.The computed Boltzmann system.C Size notion. Shallowness.Formal z parameter.The computed Boltzmann sampler.D Size notion. Shallowness. Singularity approximation error.)The computed rejection Boltzmann sampler. :;<=>?@ABCD >?@AB:;<=CD:;<=>?@ABCD+Boltzmann samplers for random lambda terms.(c) Maciej Bendkowski, 2017BSD3maciej.bendkowski@tcs.uj.edu.pl experimentalSafe EFSamples a random closed h-shallow lambda term in the given size range.FaSamples a random closed h-shallow lambda term in the given size range using the IO monad. See E for more details.G<Samples a random closed lambda term in the given size range.HWSamples a random closed lambda term in the given size range using the IO monad. See G for more details.I;Samples a random plain lambda term in the given size range.JVSamples a random plain lambda term in the given size range using the IO monad. See I for more details.KSamples a random closed h-shallow lambda term in the given size range. In addition, the term has to satisfy the given predicate. See also E.LÉSamples a random closed h-shallow lambda term in the given size range. In addition, the term has to satisfy the given predicate. The IO monad is used as the source of random numbers. See also K.M…Samples a random closed lambda term in the given size range In addition, the term has to satisfy the given predicate. See also G.N¿Samples a random closed lambda term in the given size range. In addition, the term has to satisfy the given predicate. The IO monad is used as the source of random numbers. See also M.O…Samples a random plain lambda term in the given size range. In addition, the term has to satisfy the given predicate. See also I.P¾Samples a random plain lambda term in the given size range. In addition, the term has to satisfy the given predicate. The IO monad is used as the source of random numbers. See also O.bcdefghijklmEBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.FBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.GBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.HBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.IBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.JBoltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.KFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.LFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.MFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.NFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.OFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result.PFilter function to use.Boltzmann sampler to use.Outcome size lower bound.Outcome size upper bound.The monadic result. EFGHIJKLMNOP EFKLGHMNIJOPbcdefghijklmEFGHIJKLMNOPn      !"#$$%&''()*+,-./00%&122()3,4-.566%&7789,-.:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abc)lambda-sampler-1.1-B6lOEBKhECY5MtV4tc1tc5Data.Lambda.Model Data.LambdaData.Lambda.Random.OracleData.Lambda.Random.PlainSystemData.Lambda.Random.SystemData.Lambda.Random.MixedSystemData.Lambda.RandomModelzeroWsuccWabsWappWvalidnaturalbinaryweightsLambdaVarAbsAppIndexSZtoInttoIndexisClosedmaxIndexsizesizeVar $fShowLambda $fShowIndexrootsrootsHdomSingdomSingH PlainSamplersystemmodel PlainSystemabsappzeroevalboltzmannSystemboltzmannSamplerrejectionSampler$fShowPlainSystemSamplerSystemExpridxmixedBoltzmannSystem $fShowExpr MixedSampler MixedSystem shallowSystem plainSystemclosedShallowLambdaclosedShallowLambdaIO closedLambdaclosedLambdaIO plainLambda plainLambdaIOfilterClosedShallowfilterClosedShallowIO filterClosedfilterClosedIO filterPlain filterPlainIOgcd'domFunc domFuncDerivdomFuncH domFuncHDerivnewtonweights'findevalDevalHevalIevalStake' computeIdx computeSys' toProbIdxtoProbrandomPpassrandomClosedLambdarandomClosedLambda'randomClosedP'randomClosedShallowLambdarandomClosedShallowLambda' randomIndex randomIndex' randomLambda randomLambda'randomPlainIndex