Project factorisations in partial evaluation launchbury john
Rating:
7,4/10
178
reviews

Congruence 33 understood to have terminated with value v whenever nx p, v — p, v. Applications intermediate language and to form an interpretive tower, where each language interprets the one above. For Chapters 5 and 7 a little category Preface xi theory is useful but, again, nothing too deep. Making the recursive call residual, we obtain the following residual program. We repeatedly select and remove an element from the pending list. Each of the others correspond directly with commands.

Categorically speaking, dependent sum is a Grothendieck construction where the underlying domain is viewed as a category. Those actions are performed during partial evaluation. We consider an application of supercompilation to the anal-ysis of counter systems. Initially the new residual functions are named by the original function name together with the values of the static parameters. Each finite domain FinProjx is defined by the inference rules below. Suppose that the program takes two arguments and that we want to specialise it to its first argument.

Indeed infinite structures are a popular and powerful programming method in lazy languages. If the partial evaluator is self-applicable, program generators can be made. Primitive operators may also be annotated. It is clear what it means to index by a set, but a domain has more structure and this should be taken into account. John Hughes has been my supervisor for the duration of my Ph. For any such projection, we can give a corresponding construction of its complement.

Similar principles may be seen at work in the following speculative examples. We can take one final step. A less successful result occurs with the Union type. Congruence is defined in terms of a control structure and a program division. Rather than insist that V, and Vi are actually subdomains of V it is sufficient for them to be isomorphic to sub-domains.

Surprisingly, Mogensen found that even if only one view was required, it proved to be faster to specialise the ray-tracer and then run the specialised version, than it was to run the original. Pages can include limited notes and highlighting, and the copy can include previous owner inscriptions. We will see this idea in the functional model. In each case the mix parameter remains unchanged. Blocks are sequences of statements, represented as lists. We will write either or 1 to denote this type.

Congruence and Finiteness 21 This insight defines what is essentially a new binding-time. In particular, we are able to pinpoint static values within data structures containing both static and dynamic parts. Partial Evaluation in Practice with appropriate definitions for the types Ident and Exp we will consider integer expressions only and represent booleans as integers. The expression evaluator eval uses the state to supply values for variables. The difference between these different greatest lower bounds becomes irrelevant when we introduce particular finite domains of projections, as in these domains, the usual greatest lower bound of any set of projections from these domains is itself a projection and, moreover, also a member of the same finite domain.

Without binding-time annotations, this information is dynamic. What is more, in quiet periods the inference engine could be specialised to the new set of 1. We will leave a discussion of the motivation for these choices until the conclusion. This is rarely serious because most optimisers may be switched off with little loss—they often give only a marginal improvement anyway. We use {pattern} to signify zero or more repetitions. We need a framework for reducing the general case to the canonical case. The concept of language extension can be taken further.

A source semantic definition has two parts: A set of semantic equations mapping source programs into terms of the algebra, and an interpretation which gives concrete definitions of the state and the elementary actions on it. We propose to define the main supercompilation algorithm in terms of abstract operations, which hide the details of the object language. After all, that is the range of their definition in the program. The equations are consequences of the S-m-n theorem of recursive function theory. Thus, the size of the residual program will be linear in the size of the input program. In other words, D We have seen, at least in principle, that projections may be used to provide descriptions of program values, pinpointing which parts are static.