Program operators for composing abstractions Number:7,146,604 from the United States Patent and Trademark Office (PTO) owispatent Programming abstractions with at least one expression are composed to a single abstraction using a composition operator. Expressions from the abstractions are unfolded by removing the prefix of each abstraction and substituting formal parameter names in each expression with a common parameter name to define open variables. The unfolded expressions are transformed to a reduced expression using a composition pattern that tunes semantics of the composition operators. The reduced expression is nested in the single abstraction by: appending a selected prefix of the composed abstraction to the reduced expression, binding the open variables of the reduced expression to the formal parameter of the selected prefix, and computing the type of the formal parameter of the selected prefix.<H abstractions, composing, Program, operato, 7146604.html, Patent, pto, 7146604

Title: Program operators for composing abstractions

Abstract: Programming abstractions with at least one expression are composed to a single abstraction using a composition operator. Expressions from the abstractions are unfolded by removing the prefix of each abstraction and substituting formal parameter names in each expression with a common parameter name to define open variables. The unfolded expressions are transformed to a reduced expression using a composition pattern that tunes semantics of the composition operators. The reduced expression is nested in the single abstraction by: appending a selected prefix of the composed abstraction to the reduced expression, binding the open variables of the reduced expression to the formal parameter of the selected prefix, and computing the type of the formal parameter of the selected prefix.

Patent Number: 7,146,604 Issued on 12/05/2006 to Vion-Dury

Inventors: Vion-Dury; Jean-Yves (Saint-Ismier, FR)
Assignee: Xerox Corporation (Stamford, CT)

Appl. No.: 10/248,286

Filed: January 6, 2003

Current U.S. Class: 717/120

Current International Class: G06F 9/45 (20060101)

Field of Search: 717/120

References Cited [Referenced By]

U.S. Patent Documents


6308187	October 2001	DeStefano
6374402	April 2002	Schmeidler et al.
6473895	October 2002	Lopes et al.
2002/0089541	July 2002	Orbanes et al.
2004/0148592	July 2004	Vion-Dury

Other References

L Cardelli and P. Wegner, "On understanding data types, data abstraction, and polymorphism", in ACM Computing Surveys, 17:471-522, Dec. 1985. cited by other .
Circus-DTE Factsheet, available on the Internet at http://alphaave.com/staging/Xerox/Circus-DTE/tutorial/factsheet.pdf, in 2002. cited by other .
Circus-DTE Tutorial, available on the Internet at http://alphaave.com/staging/Xerox/Circus-DTE/tutorial/tutorial.pdf in 2002. cited by other .
J. Magee, J. Kramer, and N. Dullay, "Darwin/mp: An environment for parallel and distributed programming", in proceedings of 26th HICSS, vol. II (Software Technology), Jan. 1993. cited by other .
R. Milner, "Operational and Algebraic Semantic of Concurrent Processes", in vol. 2, chapter Chap. 19, Handbook of Theoretical computer Science. Elsevier Publishers B.V., 1990. cited by other .
G. D. Plotkin, "A structural approach to operational semantics", in Technical Report DAIMI-FN-19, Computer Sciences Dept, Arhus university, Denmark, 1981. (available on the Internet at http://www.dcs.ed.ac.uk/home/gdp/publications/). cited by other .
M. Shaw, "Procedure calls are the assembly language of systems interconnection: Connectors deserve first-class statues", in Proceedings of the Workshop on Studies of Software Design, May 1993. cited by other .
Eugene Shcherbatyuk, "A language extension for programming abstractions without objects", Oct. 29, 2001, published on the Internet at http://www.modulaware.com/mdlt/mdlt84.htm. cited by other .
"Towards The Clarification Of The Object-Oriented Concepts", available on the Internet at http://www.doc.mmu.ac.uk/STAFF/J.Gray/oopslang/aoblnts/intro/OOPCONCP.HTM- , in 2002. cited by other .
U.S. Appl. No. 10/046,314, entitled "Symmetrical Structural Pattern Matching" (D/A0858). cited by other .
U.S. Appl. No. 10/046,191, entitled "Bi-Valuation Of Programming Statements" (D/A0858Q). cited by other.

Primary Examiner: Chavis; John

Claims

The invention claimed is:

1. A method for composing programming abstractions, comprising: defining a composition operation for composing a first abstraction and a second abstraction with a selected composition operator; each abstraction having a form, a prefix, and at least one expression; unfolding the expressions from the first and the second abstractions by: (a) removing the prefix of each abstraction, and (b) substituting formal parameter names in each expression with a common parameter name to define open variables; transforming the unfolded expressions to a reduced expression using a composition pattern that tunes semantics of the selected composition operator; selecting a prefix that depends on the selected composition operator and the form of the first abstraction and the second abstraction; the selected prefix having a formal parameter with a type; and nesting the reduced expression in a third abstraction that composes the first abstraction and the second abstraction by: (i) appending the selected prefix to the reduced expression, (ii) binding the open variables of the reduced expression to the formal parameter of the selected prefix, and (iii) computing the type of the formal parameter of the selected prefix.

2. The method according to claim 1, wherein the selected composition operator applies to operands that comprise at least one recursive functional abstraction.

3. The method according to claim 1, wherein the selected composition operator is as defined by: .times..times..times..times..times..function..times..times..times..times.- .times..function..times..times..times.e.times..lamda..times..times..times.- .times..times..lamda..times..times..times..times..fwdarw..lamda..times..ti- mes..times..times.e.times. ##EQU00040## where: ".lamda.x.sub.n:t.sub.n.e.sub.n" is a lambda abstraction with prefix ".lamda.x:t", in which ".lamda." identifies a form of abstraction, "x" identifies a formal parameter of type "t", and "e" is the expression of the abstraction; "e[z/x]" means substitute x.sub.n for z in the expression e.sub.n, "" means the terminal form of an operation reduces to a value, "" identifies a type combination relation, "e.sub.1e.sub.2" defines a lazy application in which the expression e.sub.2 is passed by a function without first being computed, "E" is a composition pattern.

4. The method according to claim 3, wherein the selected composition operator applies to operands that comprise at least one recursive functional abstraction.

5. The method according to claim 1, wherein the selected composition operator is as defined by: (f fresh)(.lamda.x:t.e).fwdarw.fix f(x:t)=f(e) [c3] where: ".lamda.x:t.e" is a lambda abstraction with prefix ".lamda.x:t", in which ".lamda." identifies a form of abstraction, "x" identifies a formal parameter of type "t", and "e" is the expression of the abstraction; "f" is the logical name of a function; and "fix" identifies that the expression "e" is recursive, to permit use of itself through the logical name "f".

6. The method according to claim 1, wherein the selected composition operator is as defined by: '.times..star-solid..noteq..perp..PHI..function..function..function..time- s..smallcircle..times.e.times..gradient..times..times..times..times..times- .'.gradient..times..times..times..times..times.'>.gradient..times..time- s..times..times..times.'.times..times..function.'.times..star-solid..times- . ##EQU00041## where: ".gradient.x:t,y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e" is the expression of the abstraction; ".PHI." is a parametric function that performs a syntactic transformation of n terms into a new term; "E" is a composition pattern.

7. The method according to claim 1, wherein the selected composition operator is as defined by: .PHI..function..times..smallcircle..times.e'.times..gradient..times..time- s..times..times.'>.gradient..times..times..times..times.'e'.times. ##EQU00042## where: ".gradient.x:t,y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e" is the expression of the abstraction; and ".PHI." is a parametric function that performs a syntactic transformation of n terms into a new term.

8. The method according to claim 7, wherein the selected composition operator applies to a recursive nabla abstraction.

9. The method according to claim 1, wherein the selected composition operator is as defined by: .times..gradient..times.'.fwdarw..gradient.'.function..times..times. ##EQU00043## where: ".gradient.x:t,y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e" is the expression of the abstraction.

10. The method according to claim 9, wherein the selected composition operator applies to a recursive nabla abstraction.

11. An apparatus for composing programming abstractions, comprising: means for defining a composition operation for composing a first abstraction and a second abstraction with a selected composition operator; each abstraction having a form, a prefix, and at least one expression; means for unfolding the expressions from the first and the second abstractions by: (a) removing the prefix of each abstraction, and (b) substituting formal parameter names in each expression with a common parameter name to define open variables; means for transforming the unfolded expressions to a reduced expression using a composition pattern that tunes semantics of the selected composition operator; means for selecting a prefix that depends on the selected composition operator and the form of the first abstraction and the second abstraction; the selected prefix having a formal parameter with a type; and means for nesting the reduced expression in a third abstraction that composes the first abstraction and the second abstraction by: (i) appending the selected prefix to the reduced expression, (ii) binding the open variables of the reduced expression to the formal parameter of the selected prefix, and (iii) computing the type of the formal parameter of the selected prefix.

12. The apparatus according to claim 11, wherein the selected composition operator applies to operands that comprise at least one recursive functional abstraction.

13. The apparatus according to claim 11, wherein the selected composition operator is as defined by: .times..times..times..times..times..function..times..times..times..times.- .times..function..times..times..times.e.times..lamda..times..times..times.- .times..times..lamda..times..times..times..times..fwdarw..lamda..times..ti- mes..times..times.e.times. ##EQU00044## where: ".lamda.x.sub.n:t.sub.n.e.sub.n" is a lambda abstraction with prefix ".lamda. x:t", in which ".lamda." identifies a form of abstraction, "x" identifies a formal parameter of type "t", and "e" is the expression of the abstraction; "e.sub.n[z/x.sub.n]" means substitute x.sub.n for z in the expression e.sub.n, "" means the terminal form of an operation reduces to a value, "" identifies a type combination relation, "e.sub.1e.sub.2" defines a lazy application in which the expression e.sub.2 is passed by a function without first being computed, "E" is a composition pattern.

14. The apparatus according to claim 13, wherein the selected composition operator applies to operands that comprise at least one recursive functional abstraction.

15. The apparatus according to claim 11, wherein the selected composition operator is as defined by: (f fresh)(.lamda.x:t.e).fwdarw.fix f(x:t)=f(e) [c3] where: ".lamda.x:t.e" is a lambda abstraction with prefix ".lamda.x:t", in which ".lamda." identifies a form of abstraction, "x" identifies a formal parameter of type "t", and "e" is the expression of the abstraction; "f" is the logical name of a function; and "fix" identifies that the expression "e" is recursive, to permit use of itself through the logical name "f".

16. The apparatus according to claim 11, wherein the selected composition operator is as defined by: '.times..star-solid..noteq..perp..PHI..function..function..function..time- s..smallcircle..times.e.times..gradient..times..times..times..times..times- .'.gradient..times..times..times..times..times.'>.gradient..times..time- s..times..times..times.'.times..times..function.'.times..star-solid..times- . ##EQU00045## where: ".gradient.x:t, y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e" is the expression of the abstraction; ".PHI." is a parametric function that performs a syntactic transformation of n terms into a new term; "E" is a composition pattern.

17. The apparatus according to claim 11, wherein the selected composition operator is as defined by: .PHI..function..times..smallcircle..times.e'.times..gradient..times..time- s..times..times.'>.gradient..times..times..times..times.'e'.times. ##EQU00046## where: ".gradient.x:t,y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e" is the expression of the abstraction; and ".PHI." is a parametric function that performs a syntactic transformation of n terms into a new term.

18. The apparatus according to claim 11, wherein the selected composition operator is as defined by: .times..gradient..times.'.fwdarw..gradient.'.function..times..times. ##EQU00047## where: ".gradient.x:t,y:t'.e" is a nabla abstraction with prefix ".gradient.x:t,y:t'", in which ".gradient." identifies a form of abstraction, "x" and "y" identify a parameter of type "t" and "t'" respectively, and "e " is the expression of the abstraction.

19. An article of manufacture for use in a machine, comprising: a memory; instructions stored in the memory for composing programming abstractions comprising: defining a composition operation for composing a first abstraction and a second abstraction with a selected composition operator; each abstraction having a form, a prefix, and at least one expression; unfolding the expressions from the first and the second abstractions by: (a) removing the prefix of each abstraction, and (b) substituting formal parameter names in each expression with a common parameter name to define open variables; transforming the unfolded expressions to a reduced expression using a composition pattern that tunes semantics of the selected composition operator; selecting a prefix that depends on the selected composition operator and the form of the first abstraction and the second abstraction; the selected prefix having a formal parameter with a type; and nesting the reduced expression in a third abstraction that composes the first abstraction and the second abstraction by: (i) appending the selected prefix to the reduced expression, (ii) binding the open variables of the reduced expression to the formal parameter of the selected prefix, and (iii) computing the type of the formal parameter of the selected prefix.

20. The article of manufacture according to claim 19, wherein the selected composition operator applies to operands that comprise at least one recursive functional abstraction.

Description

CROSS-REFERENCE TO RELATED APPLICATIONS

Cross-reference is made to U.S. patent application Ser. No. 10/046,314, entitled "Symmetrical Structural Pattern Matching", (now published as US 2003/0191847 A1), Ser. No. 10/046,191 entitled "Bi-Valuation Of Programming Statements", (now published as US 2003/0188297 A1), which are assigned to the same assignee as the present invention and incorporated herein by reference. Cross-reference is also made to concurrently filed U.S. patent application Ser. No. 10/248,287 entitled "Program Compiler With Abstraction Composer", (now published as US 2004/0148592 A1), which is assigned to the same assignee as the present invention and incorporated herein by reference.

BACKGROUND OF INVENTION

The present invention relates generally to software programming languages, and more particularly, to a programming language with operators adapted to compose programming abstractions.

Central to all programming languages is the concept of "programming abstractions". Programming abstractions as used herein describe functional behavior in computer programs through, for example, functions, procedures, or methods. Programming abstractions have the qualities of software code embedding, factorization, and reuse.

Code embedding refers to the use of programming abstractions (also referred to herein as "abstractions") as building blocks, where abstractions are able to call each other. Code factorization refers to the avoidance of code duplication associated with abstractions in a program. Code reuse refers to the avoidance of duplicating abstractions to develop additional functionality.

More specifically, code factorization avoids the duplication of "n" similar code segments if they are needed at "n" different locations in a software program. These different segments can be transformed into a common abstraction which can be invoked "n" times at a single location in the software program. This operation is called an abstraction because some of the programming instructions are changed in order to operate on variables instead of values. These variables constitute the execution environment of the abstraction, where the value of the variables is specified at runtime.

For example, the operation "10+1" can be abstracted into an abstraction called a .lamda.-abstraction (i.e., lambda-abstraction) that has the form ".lamda. x:int.x+1", where 10 is now defined as the variable "x" of type integer (i.e., "int"). In effect, the lambda-abstraction has generalized the operation "10+1" making it applicable to any integer, instead of a constant (e.g., 10).

Consequently if this lambda-abstraction is called "F", then F (10) will compute 11 and F (11) or F (F(10)) will compute 12.

It is therefore advantageous to define computer programs using abstractions to simplify software design by breaking down a complex monolithic program into smaller sub-programs. In addition, programming using abstractions has the additional benefit of simplifying quality assurance testing. For instance, testing a plurality of small sub-programs is easier than testing a large monolithic program because the context of each sub-program is more explicit and the branching complexity is simplified.

Besides code factorization, abstractions enable code reuse. That is, previously created abstractions can be reused when new software is developed by programmers. The reuse of abstractions may be as simple as copying abstractions from a repository of abstractions or from an existing program. In addition, the reuse of abstractions may involve the use of function previously created to create new function.

The creation of a new abstraction that combines the function of two or more existing abstractions is defined herein as the "composition of programming abstractions". Current software programming techniques are poorly adapted to facilitate the composition of abstractions in a structured and a formal manner; indeed, existing techniques achieve reuse through two basic techniques that simply reuse existing approaches for composing operators that work either by duplicating code defining abstractions or by directly calling abstractions (e.g., by nesting calls). These current techniques for composing abstractions results in the production of unnecessary code at compile time.

For example, assume an existing .gradient.-abstraction (i.e., nabla-abstraction) "P" that takes any integer "x" and computes its double as output "y" is defined as "P=.gradient.x:int, y:int.(y:=2*x)". Existing techniques for creating a new abstraction "PP" that encapsulates two subsequent calls to the abstraction "P" would be defined as "PP=.gradient.x:int, y:int.(y:=P(P(x))". Execution of the composed abstraction PP(3) would produce 12. However this method for composing abstractions could be more efficient because P(P(x)) requires more instructions than necessary to carry out the operation.

Accordingly, it would be desirable to provide a programming language and compiler adapted to compose programming abstractions. Such a programming language and compiler would advantageously speed and simplify program development and maintenance by facilitating the combination of existing abstractions in a structured and formal manner.

SUMMARY OF INVENTION

In accordance with the invention, there is provided program operators, and a compiler therefor, for composing programming abstractions. Advantageously, the program operators for composing abstractions provide a definitional framework that shows that abstractions are reused and the manner in which they are reused, simplifying program maintenance through increased legibility. In addition, the compilation of the composition of abstractions using the program operators produces a composed abstraction after compilation that is functionally equivalent to existing approaches for composing operators but computationally different, thereby increasing program efficiency at runtime.

For example, composing the existing delta-abstraction "P" (defined above) using a composition operator "pipe" (described in detail below) results in source code that defines a new abstraction as "PP'=P pipe P". This definition explicitly shows the reuse of programming abstractions in the source code. In addition after compilation, the abstraction PP' reduces to "PP'=.gradient. x:int , y: int .( var a=0.a:=2*x; y:=2*a)" which is functionally equivalent yet computationally more efficient than the abstraction PP (defined above).

In accordance with one aspect of the invention, there is provided a method, apparatus and article manufacture therefor, for composing programming abstractions. A composition operation is defined for composing a first abstraction and a second abstraction with a selected composition operator. Each abstraction has a form, a prefix, and at least one expression. The expressions from the first and the second-abstractions are unfolded by: removing the prefix of each abstraction, and substituting formal parameter names in each expression with a common parameter name to define open variables. The unfolded expressions are transformed to a reduced expression using a composition pattern that tunes semantics of the selected composition operator. A prefix is selected that depends on the selected composition operator and the form of the first abstraction and the second abstraction. The selected prefix has a formal parameter with a type. The reduced expression is nested in a third abstraction that composes the first abstraction and the second abstraction by: appending the selected prefix to the reduced expression, binding the open variables of the reduced expression to the formal parameter of the selected prefix; and computing the type of the formal parameter of the selected prefix.

BRIEF DESCRIPTION OF DRAWINGS

These and other aspects of the invention will become apparent from the following description read in conjunction with the accompanying drawings wherein the same reference numerals have been applied to like parts and in which:

FIG. 1 illustrates a general purpose computer for carrying out the present invention;

FIG. 2 illustrates a detail view of the multi-stage compiler shown in FIG. 1;

FIG. 3 illustrates a logical outline of a method for performing an abstraction composition operation shown in FIG. 2;

FIG. 4 is a flow diagram of the acts performed in the logic outline shown in FIG. 3 for carrying out the composition of abstractions;

FIG. 5 illustrates a binary tree syntactically and illustratively for encoding the arithmetic expression "a=b+10*c";

FIGS. 6 and 7 illustrate resulting binary trees syntactically and illustratively when two different transformers are applied to the binary tree shown in FIG. 5; and

FIG. 8 illustrates the resulting binary tree syntactically and illustratively when the composition of two transformers is applied to the binary tree shown in FIG. 5.

DETAILED DESCRIPTION

Outline of Detailed Description

A. Operating Environment

A.1 Multi-Stage Compiler

A.2 Method For Composing Operators

A.3 Detailed Example

B. General Syntax and Operational Semantics

C. Type System

C.1 Defining Sub-Type Relations

C.2 Typing Rules For Defining Well Typed Properties of Terms

D. The Composition of Functional Abstractions

D.1 Typing Of Composition Operators

D.2 Computational Equivalence

D.3 Application To The Computation Of Numerical Series

D.4 Handling Subtype Polymorphism (Generalization)

E. Extending the Calculus with Imperative Expressions

E.1 Computing Environment

E.2 Syntactic Expressions

E.3 Operational Semantics

E.4 Type System

F. Polymorphic Composition of Nabla-Abstractions

F.1 Semantics

F.2 Typing

G. A Set of Composition Operators

H. Safety Properties Of The Calculus

H.1 General Type Preservation Property

H.2 Strong Type Soundness Of The Core Calculus

H.3 Weak Type Soundness Of The Whole Calculus C/F(E)

I. Polymorphic Composition of Records

I.1 Definition

I.2 Using Record Polymorphism In Pam Composition

J. Illustration of a Modeling Tree Transformer

K. Miscellaneous

A. Operating Environment

FIG. 1 illustrates a general purpose computer 110 for carrying out the present invention. The general purpose computer 110 includes hardware 112 and software 114. The hardware 112 is made up of a processor (i.e., CPU) 116, memory 118 (ROM, RAM, etc.), persistent storage 120 (e.g., CD-ROM, hard drive, floppy drive, tape drive, etc.), user I/O 122, and network I/O 124. The user I/O 122 can include a keyboard 126, a pointing device 128 (e.g., pointing stick, mouse, etc.), and the display 130. The network I/O 124 may for example be coupled to a network 132 such as the Internet.

The software 114 of the general purpose computer 110 includes an operating system 136, a source code editor (and debugger) 138, and a multi-stage compiler 140. The operating system 136 permits processor 116 to allow a user of the general purpose computer 110 to compose source code using the source code editor 138. The source code, which is stored in either memory 118 or persistent storage 120, is compiled by the multi-stage compile 140.

A.1 Multi-Stage Compiler

FIG. 2 illustrates a detail view of the multi-stage compiler shown in FIG. 1. The multi-stage compiler includes a tokenizer 206, a parser 208, an importer 210, a type checker 212, a composer 214, a partial evaluator 215, an intermediate format generator 216 that generates intermediate code 220, a code optimizer, and a code generator 218 that generates executable code 204, the details of which are described below.

The multi-stage compiler 140 takes as input source code 202 and produces as output executable code 204. The multi-stage compiler may either operate statically (i.e., during a composition or analysis stage of language processing) or dynamically (i.e., during execution of the executable code). The code generator 218 may produce: executable code that constitutes machine specific operating instructions (i.e., op-codes), byte-codes that may be executed on an interpreter, or a combination of op-codes or byte-codes.

In accordance with the invention, the source code 202 is formulated with at least one abstraction composition operation 222 using for example the source code editor 138, which may be any conventional text editing program. In general, the abstraction composition operation that is defined in the source code 202 composes at least a first abstraction 224 and a second abstraction 226 using a composition operator 228.

During compilation of the source code 202, the composer 214 in the multi-stage compiler 140 reduces the abstraction composition operation 222 to a new abstraction 230. The composed abstraction 230 is later compiled into an executable form by the other elements of the multi-stage compiler 140 as described in more detail below.

In operation, the multi-stage compiler 140 receives as input source code 202 that is formulated with at least one instruction composing two abstractions (e.g., as shown at 222). Recognition of the contents of the source code is broken into two stages. Initially, the tokenizer 206 segments the source code into a sequence of tagged segments. The tagged segments are used by the parser 208, which is concerned with the structure of the source code, to build a concrete tree. The resulting concrete tree is in computable form and contains all of the useful information forming part of the source code that is necessary to formulate executable or intermediate code.

After tokenizing and parsing at 206 and 208, elements referred to in the source code that are external to the source code are resolved by the importer 210 by accessing the intermediate code 220. Subsequently, the type checker 212 applies a type checking process to the concrete tree. The type checking process traverses an abstract representation (i.e., an abstract tree) of the concrete tree, possibly in multiple passes, and decorates the abstract tree with types that add information related to the type of expressions on the abstract tree using the parsing and tokenizing information to define a decorated tree. In addition, the type checker 212 determines whether an expression is "well typed", using known methods for type checking that allows finding, legitimizing, and propagating types.

The type checker 212 delegates the processing of abstraction composition operations (e.g., abstraction composition operation 222) that are on the decorated tree to the composer 214. Thus, when the type checker 212 detects that some expressions in the source code are defined through composition operators, the type checker 212 passes the decorated tree for processing by the composer 214. The composer 214 reduces the abstraction composition operation 222 on the decorated tree into a new composed abstraction 230 that is decorated with types.

The new expressions and types added to the decorated tree by the composer 214 are then evaluated by the type checker 212 to determine whether those new expressions are well typed. In accordance with the invention, the composition of two abstractions may take place if the resulting composition is well typed. The type system described herein defines a framework for determining whether a composed expression is well typed as defined below. Generally, a well-typed expression satisfies a weak type soundness property, which provides that each transition step preserves typing.

The type checker 212 has the ability to accept subtypes and uses the type system defined below to distinguish the typing of abstractions. For example, the type system distinguishes between non-recursive and recursive abstractions. The advantage of distinguishing between these two types of abstractions is that it increases the precision of the type checking system, thereby allowing the type checker 212 to assert that the composed abstraction 230 is the correct composition of the abstraction composition operation 222.

Once all composition operations have been processed and determined to be well typed, the type checker 212 passes the decorated tree to the partial evaluator 215 which pre-evaluates language instructions in the decorated tree to reduce their complexity. The decorated tree is then evaluated by the intermediate format generator 216 to generate intermediate code 220 (i.e., a linear form of the decorated tree) for later importation by other programs. In addition, the decorated tree is evaluated by the code optimizer 217, which further evaluates the language instructions in the decorated tree to optimize certain aspects (e.g., new syntactic figures that may issue from the composition operation). Advantageously, the optimization performed by the code optimizer 217 takes place after composition by the composer 214, thereby further optimizing any composed abstractions it generates. The decorated tree is then input to the code generator 218 to generate executable code 204 (i.e., object code) for execution, for example, by processor 116 of the general purpose computer 110.

It will be appreciated by those skilled in the art that functional languages (e.g., ML family), which do not use explicit typing, may use the composition operators described herein without having to specify type operations. In an alternate embodiment of the multistage compiler 140, the type of expressions is deduced entirely from the expressions themselves using a modified type checker that guesses (i.e., infers) the best types. In this alternate embodiment, the multi-stage compiler 140 accommodates such functional languages by having the modified type checker reevaluate the decorated tree after being processed by the composer 214 to re-infer types.

A.2 Method for Composing Operators

FIG. 3 illustrates a logical outline of a method for performing the abstraction composition operation 222 shown in FIG. 2 that is performed by the composer 214. FIG. 4 is a flow diagram of the acts performed in the logic outline shown in FIG. 3 for carrying out the composition of a plurality of abstractions. FIGS. 3 and 4 are referred to simultaneously below.

Initially at 402 in FIG. 4, a composition operation that composes a plurality of abstractions with a composition operator is defined as shown in FIGS. 2 and 3 at 222. It will be appreciate that the composition operation 222 could include two or more abstractions that are composed according to one or more composition operators.

Composition operators are defined below using the symbols: , , , , and . Each composition operator may have a subscript "E" (e.g., .sub.E) that defines a "composition pattern" that is used to tune the semantics of the composition operator. The absence of the composition pattern "E" in the subscript of a composition operator (e.g., ) indicates that the composition pattern "E" is an identity pattern (i.e., no tuning is performed to the semantics of the composition operator).

In addition, the composition operator may specify a "type combination relation" in its superscript. The type combination relation describes the manner in which parameter types of the composition operator are to be combined. One type combination relation is specified for each parameter defined by the composition operator. Each type combination relation specified indicates how to determine the type a parameter of the composed abstraction will take. As defined herein, the type combination relation is defined using the symbols .sym., which represents the lowest common subtype, and , which represents the greatest common subtype, and the symbols * and .diamond., that range over {.sym., }. The absence of either of these symbols in the superscript of a composition operator indicates that the types during the composition of the parameters do not change.

At 404 in FIG. 4, each expression (e.g., 302 and 304) in each abstraction (e.g., 224 and 226) defined in the abstraction composition operation 222 are unfolded. Unfolding an expression from an abstraction involves: (a) removing the prefix of the abstraction and (b) substituting formal parameter names in each expression with a common (i.e., fresh) parameter name to define open variables. In some embodiments, the formal parameter names may be substituted for more than one common parameter name. Act 404 in FIG. 3 is illustrated in FIG. 3 by unfolding the expressions 302 and 304 into the expressions 306 and 308, respectively.

At 406 in FIG. 4, the unfolded expressions (e.g., expressions 310) are transformed to a reduced expression (e.g., reduced expression 312) using a composition pattern that tunes the semantics of the composition operator. In some instances, this transformation may introduce information that specifies how to combine parameter types. Also in some instances, this transformation may involve using a composition pattern that is an identity pattern.

At 408 in FIG. 4, a prefix is selected (i.e., the selected prefix) that depends on (a) the composition operator and (b) the form of the plurality of abstractions. Abstractions may take one of four forms: a .lamda.-abstraction, a .gradient.-abstraction, and their recursive variants (which are all defined in detail below). The selected prefix has at least one formal parameter with a type.

At 410 in FIG. 4, the reduced expression (e.g., reduced expression 312) is nested in a composed abstraction (e.g., composed abstraction 308) by: (a) appending the selected prefix (selected at act 408) to the reduced expression; (b) binding the open variables of the reduced expression (introduced at act 404) to the formal parameter of the selected prefix; and (c) computing the type of the formal parameter of the selected prefix in accordance with the type combination relation specified for the composition operator.

A.3 Detailed Example

The following example illustrates the composition of two abstractions Abs1 and Abs2 using the composition operator defined at [c1] below as:

.times..times..times..function..function..times..function..function..times- ..times..times..times..times..lamda..times..times..times..lamda..times..ti- mes..fwdarw..lamda..times..times..times..times..times. ##EQU00001## where:

".lamda.x.sub.n:t.sub.n.e.sub.n" is a lambda abstraction with prefix ".lamda.x:t", in which ".lamda." identifies a form of abstraction, "x" identifies a formal parameter (i.e., a parameter encapsulated in an abstraction) of type "t", and "e" is the expression of the abstraction,

"e.sub.n[z/x.sub.n]" means substitute x.sub.n for z in the expression e.sub.n,

"" means the terminal form of an operation (i.e., after possibly several operational steps) reduces to a value,

"" identifies a type combination relation that specifies the greatest common subtype relation,

"e.sub.1e.sub.2" defines a lazy application in which the expression e.sub.2 is passed by a function without first being computed, and

"E" is a composition pattern (i.e., a lambda term that parameterizes the composition operation .sub.E(e.sub.1, . . . , e.sub.n)).

Assuming in this example the lazy application "e e" is given by a [.beta..sub.1] reduction defined as: .lamda.x:t.e.sub.1e.sub.2.fwdarw.e.sub.1[e.sub.2/x] [.beta..sub.1]

Also assuming in this example that the abstractions Abs1 and Abs2 are given by: Abs1.ident..lamda.x:any .x(where x is a formal parameter of type "any"), and Abs2.ident..lamda.x:int. 1 (where x is a formal parameter of type "int").

Further assuming in this example that the composition pattern "E" of the composition operation .sub.Sub is given by: Sub.ident..lamda.x:int..lamda.y:int.x-y

Given the above assumptions, the composition of the abstractions Abs1 and Abs2 is expressed as (i.e., at act 402 in FIG. 4): .sub.Sub(Abs1, Abs2)=.sub.Sub (.lamda.x:any .x, .lamda.x:int. 1).

Initially the expressions e of each abstraction are unfolded in accordance with the general form Ee.sub.1[z/x.sub.1] . . . e.sub.n[z/x.sub.n] by (a) removing the prefix (e.g., ".lamda.x:any" and ".lamda.x:int") of each abstraction (i.e., at act 404(1) in FIG. 4) and (b) substituting the formal parameter name "x" in each expression with a common (i.e., fresh) parameter name "z" to provide the unfolded expression (e.g., (i.e., at act 404(2) in FIG. 4): Subx[z/x]1[z/x'].

Transforming the unfolded expression using the composition pattern Sub provides a reduced expression (i.e., at act 406 in FIG. 4) initially in the form (after substituting "x" for "z" in the expression "e" given by "e[z/x]"):

Subz1, which after expanding in accordance with the composition pattern Sub provides:

.lamda.x:int.y:int.x-yz1, which after applying z to x in accordance with [.beta..sub.1] reduction reduces to:

.lamda.y:int.z-y1, and which after applying 1 for y in accordance with [.beta..sub.1] reduction reduces to the reduced expression (called "e"): z-1.

A prefix is selected with a value that depends on the composition operator (e.g., ) and the form of the plurality of abstractions (e.g., Abs1 and Abs2). For this example the selected prefix is ".lamda.x:???" (i.e., at act 408 in FIG. 4). Finally, the reduced expression is nested in an abstraction by appending the selected prefix (i.e., at act 410(1) in FIG. 4) as follows:

.lamda.x:???.z-1, and binding the open variable "z" to the formal parameter "x" of the selected prefix (i.e., at act 410(2) in FIG. 4) as follows:

.lamda.z:???.z-1, and computing the type of the formal parameter of the selected prefix in accordance with the greatest common subtype relation of types "any" and "int" (e.g., any int.ident.int) (i.e., at act 410(3) in FIG. 4) as follows to provide the composed abstraction: .lamda.z:int.z-1. B. General Syntax and Operational Semantics

Operational semantics is described herein using the SOS style described in G. Plotkin's article "A structural approach to operational semantics", Technical Report DAIMI-FN-19, Computer Sciences Dept., .ANG. rhus university, Denmark, 1981, considering "small step" transitions in order to cover an eventual extension to concurrent languages with interleaving semantics.

A set of definitions is provided of a general abstract syntax of expressions "e" that describes basic constructs for terms of the underlying programming language, where the notation of "e" encompasses imperative and functional expressions. The first set defined in this section specifies functional expressions and the second set defined below in section E specifies imperative expressions.

An "imperative expression" as used herein generally means an expression that involves several sequential computational steps. A "functional expression" as used herein generally means an expression that allows "functional style" programming (i.e., programming that allows solution of problems to be found by defining functions and applying parameters to those functions).

Functional expressions "e", with types "t", defined herein include:

TABLE-US-00001 e ::= n | x | s | numerical values, variables, string litterals e*e | basic operations (* .epsilon. {+, -, *}) if e then e else e | alternation .lamda.x:t.e | fixf(x:t)=e | typed lambda abstraction and recursive variant e(|e|) | e(e) | lazy and strict application e ::= true | false | boolean literals e == e | e > e | comparisons t ::= int | string | bool | primitive types t|t | union of types T | .perp. | t .fwdarw. t | t t top and bottom type, functions, recursive functions

The definition of two different applications are described herein: the first definition of "application" (i.e., e.sub.1e.sub.2) allows lazy application whereas the second definition of "application" (i.e., e.sub.1(e.sub.2)) allows strict application (i.e., where the parameter must be normalized to a value before substitution, where a value is defined herein as a Boolean or numerical literal, or a (recursive) lambda abstraction).

As used herein, a transition system describes an interpreter of the language through a transition relation which defines the computation of any expression e into a new expression e', and is noted e.fwdarw.e'. Also, several computation steps such as e.fwdarw.e'.fwdarw.e'' are abbreviated herein using the notation ee''. Normalizing computations will reduce the expression e to a term e' which cannot be further reduced; this particular computation step is noted ee' and formally defined by:

.fwdarw.'.times..times.'.times..fwdarw..times..times.'.function. ##EQU00002##

By convention, values are noted v or n, s if they are numeric or string constants. A derivation chain that reduces to a value is noted ev. The notation ee' is used herein for derivation paths of zero or more steps transforming e in e'.

The following equations define the testing operation semantics: if true then e.sub.2 else e.sub.3.fwdarw.e.sub.2 [if1] if false then e.sub.2 else e.sub.3.fwdarw.e.sub.3 [if2]

.fwdarw.'.times..times..times..times..times..times..times..times..times..t- imes..fwdarw..times..times.'.times..times..times..times..times..times..tim- es..times..times..times. ##EQU00003##

The semantics of operations on basic types is without surprise defined as (where the meta symbol is given by *.epsilon.{+,-,*,>,==}, and where .sup..epsilon. evaluates numeric literals into integer):

.fwdarw.'.times..star-solid..times..times..fwdarw.'.times..times..star-sol- id..times..times..function..times. .star-solid. ##EQU00004## .fwdarw.'.upsilon..times..times..star-solid..times..times..fwdarw..upsilo- n..times..times..star-solid..times..times.'.function..times. .star-solid. ##EQU00004.2## .function..function..function..fwdarw..function. ##EQU00004.3## .fwdarw..times..function. ##EQU00004.4## .function..function..times..function..fwdarw..function. ##EQU00004.5## .function..function..function..fwdarw..function. ##EQU00004.6##

Note for the definitions [eq] and [neq] below, the symbol "=.sup..alpha.", which is known as alpha-equivalence in the lambda calculus theory, is the syntactic equality, up to alpha-substitution (as set forth at the beginning of section D.2 below).

.upsilon..times..alpha..times..upsilon..upsilon..upsilon..fwdarw..times..t- imes. .upsilon..times..alpha..times..upsilon..upsilon..upsilon..fwdarw..ti- mes..function.>.function.>.fwdarw..function..function..ltoreq..funct- ion.>.fwdarw..times. ##EQU00005##

Both lazy and strict application evaluate left argument first:

.fwdarw.'.function..fwdarw.'.times..times..function. ##EQU00006## .fwdarw.'.function..fwdarw.'.times..times..function. ##EQU00006.2##

The strict application requires (a) a normalized left term and (b) evaluating the parameter before substitution, while lazy application substitutes terms directly.

.fwdarw.'.upsilon..function..fwdarw..upsilon.'.times..function. ##EQU00007## .lamda.x:t.e.sub.1(v).fwdarw.e.sub.1[v/x] [.beta..sub.2] .lamda.x:t.e.sub.1e.sub.2.fwdarw.e.sub.1[e.sub.2/x] [.beta..sub.1]

Application on recursive abstractions "f" is performed towards two substitutions: the rewriting of the recursion variable by the recursive abstraction itself and then the usual substitution of the parameter. fixf(x:t)=e(v).fwdarw.e[fixf(x:t)=e/f][v/x] [.beta..sub.3]

As usual in lambda calculi, the substitution operation involved in [.beta..sub.1], [.beta..sub.2] and [.beta..sub.3] must avoid name capture.

C. Additional Type System

Composition operators operate over types. The typing rules set forth below define well typed properties of types. In one embodiment, the type checker 212 includes instructions that determine whether an expression is well typed using a series of logical operations that verify whether an expression is weakly sound in accordance with the typing rules defined herein.

C.1 Defining Sub-Type Relations

Accordingly, this section defines sub-type relations (i.e., subtype properties of types). That is, this section defines how types propagate during composition. More specifically, this section presents a formal type system including a (reflexive and transitive) subtype relation t.sub.1t.sub.2 (which provides t.sub.1 is a subtype of t.sub.2), with basic axioms for all type t and expression e. The subtype relations [top] and [bot] are defined as: tT[top].perp.t [bot]

Typing assertions are noted herein as e:t (i.e., expression e has type t). A typing environment .gamma. may contain typing assertions over variables, and is used through the .gamma.e:t notation, where "" provides that expression e has type t in environment .gamma.. Typically environment .gamma., x:t means that the current environment contains the assertion that variable x has type t. The typing assertion [sub] is defined as:

.gamma. .times..times. .gamma. .times. ##EQU00008##

The proposed notations distinguishes between "exact" typing (e::t) and typing by subsumption (e:t). This allows more precise type control, thereby avoiding over generalizing influences due to so called subsumption rule (see [sub] above), while preserving the convenience of subtyping mechanism. The union type provides a simple way to construct a super type by aggregating two types.

.gamma. .gamma. .function..times. .times..times. .times. .function..times..times. ##EQU00009## .times..function..times..times..times..times. .times..function..times..times. ##EQU00009.2##

The proposed type system makes use of two relations over types.

Definition 1: Greatest common subtype .

Let be the language generated by the grammar of types, where is a total mapping from .times. into such that:

.A-inverted.t.sub.1, t.sub.2t.sub.1t.sub.2 is the greatest common subtype of t.sub.1 and t.sub.2.

Definition 2: Lowest common supertype .

Let be the language generated by the grammar of types, where is a relation from .times. into such that:

.A-inverted., t.sub.2t.sub.1.sym.t.sub.2 is the greatest common subtype of t.sub.1 and t.sub.2.

Note that common subtypes or super types always exist because of the definition of T and .perp. types. The .sym. relation (used for instance in the [If] rule) is more abstract than the type union, since for instance int .sym. string is either int|string or int|string|int. The [If] rule allows therefore precise and flexible typing of conditional statements, and the same for lambda abstractions (i.e., rules [f2,f2b] and [Fix,Fixb]).

The structural equality allows a natural treatment of types and their properties.

Definition 3: Structural type equality. t.sub.1=t.sub.2 t.sub.1t.sub.2 and t.sub.2t.sub.1

C.2 Typing Rules for Defining Well Typed Properties of Terms

The following set of typing equations covers additional logical assertions needed to handle the static semantics of the defined calculus (*.epsilon.{+,-,*}). (Note that indicates that no typing context information is necessary.) .0.true::bool [b1] .0.false::bool [b2] .0.n::int [i] .0.s::string [s] .gamma., x:tx::t [var]

.times..times. .fwdarw. .fwdarw..times. .times..times. .fwdarw. .fwdarw..function..gamma. .times..times..gamma. .times..times..gamma. .gamma. .times..times..times..times..times..times..times..times..times..t- imes. .sym..times..gamma. .times..times..gamma. .gamma. .times..gamma. .times..times..gamma. .gamma. .times..star-solid..times..times. .times. .star-solid..gamma. .times..gamma. .gamma. .function. .gamma. .times..times..gamma. .gamma. > .times. ##EQU00010##

The typing of abstraction and application can be classically handled through the following equations. (Note also that the meta symbol in [a] ranges over symbols .fwdarw. and .)

.function..gamma..times..times..gamma. .gamma. .lamda..times..times. .fwdarw..function..gamma..times..times..gamma..times..times. .gamma. .times..times..times..function. .times..times..gamma. .fwdarw..times..times..gamma. .gamma. .function. .gamma. .fwdarw..times..times..gamma. .gamma. .function. ##EQU00011##

The precise typing of some functional abstraction A.lamda.x:int|string.x+x is not possible through this conventional approach, although it is correct from the execution point of view. This expression is defined herein as type int|string.fwdarw.int|string since A(10) 20 and A(`10`) `1010`. In addition, the following is asserted as well A(10):int and A(`10`):string. The following sets of equations provide more typing power both for non-recursive and recursive abstractions (where in the equation [Fix.sup.+]t.sub.ij.epsilon.{t.sub.1, . . . , t.sub.n} and all distinct, and in the equation [a.sup.+]i.sub.1, . . . , i.sub.k .epsilon.[1,n] and all distinct).

.function..gamma..times..times..gamma. '.times..times..times..times..gamma. '.gamma. .lamda..times..times..times..times. .fwdarw.'.sym..sym..fwdarw.'.sym..times..times..fwdarw.'.times..times.'.f- unction..gamma..times..times..gamma..times..times.' .times..times.'.times..times..times..times..gamma..times..times.' .times..times.'.gamma. .times..times..function..times..times..times..times..times..times.'.sym..- sym..times..times.'.sym..times..times..times..times.'.times..times.'.gamma- . .fwdarw.'.times..times..times..fwdarw.'.times..gamma. .times..times..times..times..gamma. .times. .times..gamma. .times..times..times..times..times..times..gamma. .times..times..gamma. .function. '.sym..times..times..sym..times..times.'.gamma. .fwdarw..times..times..fwdarw.'.times..times..gamma. .times..times..times..times..times..times..gamma. .gamma. .function. .times..times.'.sym..times..times..sym.' ##EQU00012## D. The Composition of Functional Abstractions

The composition of abstractions specified in this section are performed through: an n-ary (parametric) operator that follows the syntax .sub.E(e.sub.1, . . . , e.sub.n), where E is a lambda term that parameterizes the operation; and one unary operator (e). The semantics of the first composition is defined by the following three rules [c0], [c1], and [c2]:

.fwdarw.'.times..times..times..fwdarw..times..times.'.times. ##EQU00013##

Rule [c0] shows that each operand is normalized, following a left to right order. The next rule [c1] shows how the operator reduces to its terminal form when all operands are normalized to lambda abstractions as follows:

.times..times..times..function..function..times..function..function..times- ..times..times..times..lamda..times..times..times..lamda..times..times..fw- darw..lamda..times..times. ##EQU00014##

The composition of (at least) one recursive lambda abstraction produces a recursive lambda abstraction reduced to its terminal form as follows in rule [c2]:

.times..times..times..function..function..times..function..function..times- ..times..times..times..function..times..times..times..times..lamda..times.- .times..times..times..times..times..times..lamda..times..times..fwdarw..ti- mes..times..times..times..times..times. ##EQU00015##

The semantics of the second operator are defined by the following two rules [c3a] and [c3]:

.fwdarw.'.times..fwdarw..times.' ##EQU00016## (f fresh) (.lamda.x:t.e).fwdarw.fix f(x:t)=f(e) [c3]

D.1 Typing of Composition Operators

The composition operators are typed as follows (note that in this and other typing sections the symbol ".fwdarw." means returns, where in other sections not concerning typing, it means transforms):

.di-elect cons..times..gamma. '.fwdarw..fwdarw.'.fwdarw..times..times..gamma. .fwdarw.'.gamma. .times..times. .fwdarw..times..times. ##EQU00017##

For all i, j .epsilon.[1,n], i.noteq.j:

.gamma. '.fwdarw..fwdarw.'.fwdarw..times..times..gamma. .fwdarw.'.times..times..gamma. .times..times.'.gamma. .times..times. .times..times..times..times. ##EQU00018##

.gamma. .fwdarw..gamma. .times. .times..times. ##EQU00019##

D.2 Computational Equivalence

This section defines an equivalence over terms of the calculus defined herein, noted ".about.", up to .alpha.-equivalence "=.sup..alpha." (i.e., two terms are .alpha.-equivalent if there exists a substitution which brings the terms to syntactic equality).

Definition 4: Computational Equivalence ".about." is given by: e.sub.1.about.e.sub.2 iff e.sub.1v.sub.1 and e.sub.2v.sub.2 and v.sub.1=.sup..alpha.v.sub.2

It may be shown that ".about." is an equivalence relation, i.e., reflexive, symmetric and transitive (assuming that "=.sup..alpha." is an equivalence relation also).

D.3 Application to the Computation of Numeric Series

This section provides examples of the application of composition operators to the computation of numeric series. Consider the recursive function "Fact" which computes the factorial product of any positive integer "x" as follows: Fact fix f (x:int)=if x>1 then x*f(x-1) else x

Applied to 4, "Fact" returns 4!=4.times.3.times.2.times.1 (i.e., Fact (4)24). In addition, consider the following functions "S" and "Fibo" (which computes the Fibonacci number of rank "x"): Sfix f(x:int)=if x>1 then x+f(x-1) else x Fibofix f(x:int)=if x>1 then f(x-2)+f(x-1) else x

Considering now the function "S" which applied to 4 returns 4+3+2+1 (i.e., S(4)10), it can be observed there exists a strong similarity between the structure of the code for the functions "Fact" and "S". In addition, a similar structure for the code can be observed between the functions "Fact" and "Fibo".

The composition operators defined herein are advantageously adapted to capture "patterns" in the example functions (e.g., Fact, S, and Fibo) as the composition of fewer fundamental lambda abstractions, some of which are reused several times in order to build the following .about.-equivalent abstractions:

TABLE-US-00002 Id .lamda.x:int.x Add .lamda.x:int..lamda.y:int.x + y Sub .lamda.x:int..lamda.y:int.x - y Mul .lamda.x:int..lamda.y:int.x * y If .lamda.x:int..lamda.y:int.if x > 1 then y else x

Proposition 1: Is given by:

TABLE-US-00003 let A .sub.Sub(Id, .lamda.x:int.1) then A ~ .lamda.x:int.x - 1 let B .sub.Sub(Id, .lamda.x:int.2) then B ~ .lamda.x:int.x - 2

Proving proposition 1 is a straightforward application of [c1] on A and B (defined above) that result in a lambda term which cannot be further reduced and is an .alpha.-equivalent to ".lamda.x:int.x-1".

Proposition 2: Is given by:

TABLE-US-00004 .sub.If(Id, .sub.Mul(Id, (A))) ~ Fact .sub.If(Id, .sub.Add(Id, (A))) ~ S .sub.If(Id, .sub.Add( (B), (A))) ~ Fibo

In proving proposition 2, a derivation path is produced for the function "Fact" as follows:

TABLE-US-00005 .sub.If(Id, .sub.Mul(Id, (A))) .sub.If(Id, .sub.Mul(Id,fixF(z:int)=F(z - 1))) .sub.If(Id,fixF(z':int)=z' * F(z' - 1)) fixF'(z'':int)=if z'' > 1 then z'' * F'(z'' - 1) else z''

where a, b, and c correspond to: .sup.ac0.c0.c3 .sup.bc0, c2, @.sub.2, .beta..sub.1, .beta..sub.1 .sup.cc2, @.sub.2, .beta..sub.1, .beta..sub.1

Proposition 3 (which provides that during composition basic building blocks can be reused) is given by:

TABLE-US-00006 let Z .lamda.a:int .fwdarw. int .fwdarw. int..lamda.b:int .fwdarw. int .sub.If(Id, .sub.a(b, (A))) Z(Mul)(Id) ~ Fact then {open oversize brace} Z(Add)(Id) ~ S Z(Add)( (B)) ~ Fibo

It will be appreciated that the obtained reuse is "syntactic", as opposed to the functional reuse which is related to runtime factorization of program instructions. As a consequence, the result of the composition will execute as fast as the original abstraction (e.g., Fact). However, standard functional composition will not benefit from similar efficiencies, with patterns such as: fix f(x:int)=if x>1 then Mul(x)(f(Sub(x)(1))) else x

or with more abstract patterns such as: W.lamda.f:int.fwdarw.int.fwdarw.int..lamda.g:int.fwdarw.int.fwdarw.int.fi- xF(x:int)=if x>1 then f(x)(F(g(x)(1))) else x

which allows equivalent computation after installation of:

W(Mul)(Sub)(4).about.Fact(4) and W(Add)(Sub)(4).about.S(4)

In terms of computation costs, if W(Mul)(Sub)w and Z(Mul)(Id) z then w(n) computes n! through "8.times.(n-1)+1" steps versus "4.times.(n-1)+1" for z(n).

D.4 Handling Subtype Polymorphism (Generalization)

The definitions above for [c1] and [c2] require all parameters of functional abstractions to share the same type. This, however, is a little too restrictive. It would therefore be better for instance to use the definition "I.lamda.x:T.x" rather than the earlier definition ".lamda.x:int.x", since the first definition is a more general identity function. However, correct typing for the composition needs to be ensured. For example, the expression: .sub.Mul(I,.lamda.x:int.x-1)

cannot be typed (i.e., Mul:int.fwdarw.int.fwdarw.int does not yield Tint). Accordingly, the following polymorphic variants for [c1], [c2], [C-1], [C-2] (i.epsilon.[1,n], t.sup..times.=t.sub.1 . . . t.sub.n and t.sup.+=t.sub.1 .sym. . . . .sym. t.sub.n) are given by:

.times..times..times..times..function..function..times..function..function- ..times..times..times..times..sym..times..lamda..times..times..times..lamd- a..times..times..fwdarw..lamda..times..times..times..times..times..functio- n..function..times..function..function..times..times..times..times..functi- on..times..times..times..times..sym..times..lamda..times..times..times..ti- mes..times..times..times..times..lamda..times..times..fwdarw..times..times- ..times..times..times..times..gamma. '.fwdarw..fwdarw.'.fwdarw..times..times..gamma. .fwdarw..gamma. .times..sym..times..times. .fwdarw..times..times..times..times..gamma. '.fwdarw..fwdarw.'.fwdarw..times..times..times..fwdarw..lamda..times..tim- es.'.times..times..0..sym. ''.gamma. .times..sym..times..times. .sym..times..times..times..times..times..di-elect cons..noteq..times..gamma. '.fwdarw..fwdarw.'.fwdarw..times..fwdarw..times..lamda..times..times.'.ti- mes..times..0. ''.times..fwdarw..times..times..times..times.'.times..times..0..times..ti- mes.' ''.gamma.