Strictness analysis

Last updated

In computer science, strictness analysis refers to any algorithm used to prove that a function in a non-strict functional programming language is strict in one or more of its arguments. This information is useful to compilers because strict functions can be compiled more efficiently. Thus, if a function is proven to be strict (using strictness analysis) at compile time, it can be compiled to use a more efficient calling convention without changing the meaning of the enclosing program.

Contents

Note that a function f is said to diverge if it returns : operationally, that would mean that f either causes abnormal termination of the enclosing program (e.g., failure with an error message) or that it loops infinitely. The notion of "divergence" is significant because a strict function is one that always diverges when given an argument that diverges, whereas a lazy (or non-strict) function is one that may or may not diverge when given such an argument. Strictness analysis attempts to determine the "divergence properties" of functions, which thus identifies some functions that are strict.

Approaches to strictness analysis

Forward abstract interpretation

Strictness analysis can be characterized as a forward abstract interpretation which approximates each function in the program by a function that maps divergence properties of the arguments onto divergence properties of the results. In the classical approach pioneered by Alan Mycroft, the abstract interpretation used a two-point domain with 0 denoting the set considered as a subset of the argument or return type, and 1 denoting all values in the type. [1]

Demand analysis

The Glasgow Haskell Compiler (GHC) uses a backward abstract interpretation known as demand analysis to perform strictness analysis as well as other program analyses. In demand analysis, each function is modelled by a function from value demands on the result to value demands on the arguments. A function is strict in an argument if a demand for its result leads to a demand for that argument. [2]

Projection-based strictness analysis

Projection-based strictness analysis, introduced by Philip Wadler and R.J.M. Hughes, uses strictness projections to model more subtle forms of strictness, such as head-strictness in a list argument. (By contrast, GHC's demand analysis can only model strictness within product types, i.e., datatypes that only have a single constructor.) A function is considered head-strict if , where is the projection that head-evaluates its list argument. [3]

There was a large body of research on strictness analysis in the 1980s.

Related Research Articles

Fourier analysis Branch of mathematics

In mathematics, Fourier analysis is the study of the way general functions may be represented or approximated by sums of simpler trigonometric functions. Fourier analysis grew from the study of Fourier series, and is named after Joseph Fourier, who showed that representing a function as a sum of trigonometric functions greatly simplifies the study of heat transfer.

The number π is a mathematical constant. It is defined as the ratio of a circle's circumference to its diameter, and it also has various equivalent definitions. It appears in many formulas in all areas of mathematics and physics. It is approximately equal to 3.14159. It has been represented by the Greek letter "π" since the mid-18th century, and is spelled out as "pi". It is also referred to as Archimedes' constant.

Radian SI derived unit of angle

The radian, denoted by the symbol , is the SI unit for measuring angles, and is the standard unit of angular measure used in many areas of mathematics. The length of an arc of a unit circle is numerically equal to the measurement in radians of the angle that it subtends; one radian is 180/π degrees or just under 57.3°. The unit was formerly an SI supplementary unit and the radian is now considered an SI derived unit. The radian is defined in the SI as being a dimensionless value, and its symbol is accordingly often omitted, especially in mathematical writing.

Fourier transform Mathematical transform that expresses a function of time as a function of frequency

In mathematics, a Fourier transform (FT) is a mathematical transform that decomposes functions depending on space or time into functions depending on spatial or temporal frequency, such as the expression of a musical chord in terms of the volumes and frequencies of its constituent notes. The term Fourier transform refers to both the frequency domain representation and the mathematical operation that associates the frequency domain representation to a function of space or time.

Exponentiation Mathematical operation

Exponentiation is a mathematical operation, written as bn, involving two numbers, the baseb and the exponent or powern, and pronounced as "b raised to the power of n". When n is a positive integer, exponentiation corresponds to repeated multiplication of the base: that is, bn is the product of multiplying n bases:

Clean (programming language)

Clean is a general-purpose purely functional computer programming language. For much of the language's active development history it was called Concurrent Clean, but this was dropped at some point. Clean is being developed by a group of researchers from the Radboud University in Nijmegen since 1987.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

In computer science and computer programming, a function f is said to be strict if, when applied to a non-terminating expression, it also fails to terminate. A strict function in the denotational semantics of programming languages is a function f where . The entity , called bottom, denotes an expression that does not return a normal value, either because it loops endlessly or because it aborts due to an error such as division by zero. A function that is not strict is called non-strict. A strict programming language is one in which user-defined functions are always strict.

In mathematics, specifically complex analysis, the principal values of a multivalued function are the values along one chosen branch of that function, so that it is single-valued. The simplest case arises in taking the square root of a positive real number. For example, 4 has two square roots: 2 and –2; of these the positive root, 2, is considered the principal root and is denoted as

The Glasgow Haskell Compiler (GHC) is an open-source native code compiler for the functional programming language Haskell. It provides a cross-platform environment for the writing and testing of Haskell code and it supports numerous extensions, libraries, and optimisations that streamline the process of generating and executing code. GHC is the most commonly used Haskell compiler. The lead developers are Simon Peyton Jones and Simon Marlow.

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).

In mathematics, the question of whether the Fourier series of a periodic function converges to the given function is researched by a field known as classical harmonic analysis, a branch of pure mathematics. Convergence is not necessarily given in the general case, and certain criteria must be met for convergence to occur.

In mathematics, particularly in functional analysis, a projection-valued measure (PVM) is a function defined on certain subsets of a fixed set and whose values are self-adjoint projections on a fixed Hilbert space. Projection-valued measures are formally similar to real-valued measures, except that their values are self-adjoint projections rather than real numbers. As in the case of ordinary measures, it is possible to integrate complex-valued functions with respect to a PVM; the result of such an integration is a linear operator on the given Hilbert space.

Functional (mathematics) Types of mappings in mathematics

In mathematics, the term functional has at least three meanings.

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, and Idris, dependent types may help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

In mathematics, holomorphic functional calculus is functional calculus with holomorphic functions. That is to say, given a holomorphic function f of a complex argument z and an operator T, the aim is to construct an operator, f(T), which naturally extends the function f from complex argument to operator argument. More precisely, the functional calculus defines a continuous algebra homomorphism from the holomorphic functions on a neighbourhood of the spectrum of T to the bounded operators.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

Complex logarithm Logarithm of a complex number

In the branch of mathematics known as complex analysis, a complex logarithm is an analogue for nonzero complex numbers of the logarithm of a positive real number. The term refers to one of the following:

In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.

Argument (complex analysis)

In mathematics, the argument is a multi-valued function operating on the nonzero complex numbers. With complex numbers z visualized as a point in the complex plane, the argument of z is the angle between the positive real axis and the line joining the point to the origin, shown as in Figure 1 and denoted arg z. To define a single-valued function, the principal value of the argument is used. It is often chosen to be the unique value of the argument that lies within the interval (–π, π].

References

  1. Mycroft, Alan (1980). "The theory and practice of transforming call-by-need into call-by-value". Lecture Notes in Computer Science: Proc. 4th Intl. Symp. on Programming, Vol. 83. Springer-Verlag.
  2. "The GHC Commentary: Demand analyser in GHC" . Retrieved 2014-02-12.
  3. Wadler, P.; R.J.M. Hughes (1987). "Projections for strictness analysis". Functional programming and computer architecture; LNCS 274. Springer-Verlag.