Dirk Pape
Institut für Informatik
Freie Universität Berlin
email: pape@inf.fu-berlin.de
In K. Hammond and A.J.T. Davie and C. Clack (eds.), Implementation of Functional Languages (IFL '98) London, UK, LNCS 1595 , pp. 155-170, Springer Verlag, September 1998
Abstract. A new denotational semantics is introduced for realistic non-strict functional languages, which have a polymorphic type system and support higher order functions and user definable algebraic data types. It maps each function definition to a demand propagator, which is a higher order function, that propagates context demands to function arguments. The relation of this Òhigher order demand propagation semanticsÓ to the standard semantics is explained and it is used to define a backward strictness analysis. The strictness information deduced by this analysis is very accurate, because demands can actually be constructed during the analysis. These demands conform better to the analysed functions than abstract values, which are constructed alone with respect to types like in other existing strictness analyses. The richness of the semantic domains of higher order demand propagation makes it possible to express generalised strictness information for higher order functions even across module boundaries.
Get [ pdf | ps.gz ] (© Springer Verlag)
Technical Report B 98-16
Freie Universität Berlin, Department of Computer Science, October 1998Abstract. Higher Order Demand Propagation as proposed in Report B 98-15 provides a non-standard denotational semantics for a realistic functional language. This semantics can be used to deduce generalised strictness information for higher order polymorphic functions. This report provides the formal proof for the correctness of this strictness information with respect to the non-strict standard semantics.
Technical Report B 98-15
Freie Universität Berlin, Department of Computer Science, October 1998Abstract. In this report a new backward strictness analysis for functional languages is presented. It is called higher order demand propagation and is applicable to a realistic non-strict functional language, which has a polymorphic type system and supports higher order functions and user definable algebraic data types. This report defines a semantics for higher order demand propagation and relates it to the standard semantics of the functional language. Each definition in a program is mapped to a demand propagator, which is a higher order function, that propagates context demands to function arguments. The strictness information deduced by the analysis is very accurate, because demands can actually be constructed during the analysis. These demands conform better to the analysed functions than abstract values, which are constructed alone with respect to the type information like in other existing strictness analyses. The richness of the semantic domains of higher order demand propagation makes it possible to express generalised strictness information for higher order functions even across module boundaries. An approach to integrate the higher order demand propagation analysis into an existing compiler for a lazy functional language is sketched at the end of the report.
M. Pfender, M. Kröplin and D. Pape
Mathematical Structures in Computer Science (1994), vol. 4, pp. 295-313
Cambridge University Press 1994Abstract. Within a categorical framework for primitive recursion, equality between primitive recursive (p.r.) maps is shown to be definable by suitable p.r. equality predicates. Equivalence is shown between a direct categorical formalization of classical p.r. functions and p.r. maps in the sense of Lawvere and Freyd. An extension of the theory is shown to admit a
universal setcontaining all objects of the extended theory of subobjects.
Last change: 08/06/1999, Dirk Pape.