No description available.

This thesis studies various manifestations of monads in the mathematics of computation and presents three applications of calculi based on monads. The view that monads provide abstract mathematical interpretations of computational phenomena led E. Moggi to use the internal language of a category with a strong monad, which he called the computational lambda calculus, for describing denotational semantics of programming languages. Moggi argued that models of complicated forms of computation could be described modularly by using semantic constructors for manipulating monads. For the first application, we describe a theory of exceptions in the computational lambda calculus and give a computationally adequate interpretation of a fragment of ML, including the exception handling mechanism, in models of this theory. To our knowledge no other model of ML exceptions is available in the literature to date. We also show that normalization fails when exceptions are added to the simply typed lambda calculus. Building on top of the computational lambda calculus, A.M. Pitts proposed a predicate calculus to reason about the evaluation properties of programs: the Evaluation Logic. Following the tenets of synthetic domain theory, we interpret this logic in an ambient category with set-like structure and a fully reflective subcategory of domains with a monad for interpreting computation. We establish abstract conditions under which the monad extends to the ambient category to ensure good interaction with the logical structure. We also show that a monad and first order logical structure yield suitable evaluation relations, which can be used to give a standard interpretation of Evaluation Logic when higher order structure is not available. For the second application, we focus on side effects and investigate the use of Evaluation Logic in partial correctness reasoning. We show that, under fairly common circumstances, monads for side effects admit an extension to the ambient category which is more natural than that described for arbitrary monads and we validate special axioms for members of this class. The resulting theory of computation with side effects is then put to work on a textbook example of partial correctness specification. For our third application, we consider Moggi's modular approach to denotational semantics. We develop the theory of this approach by determining which equations are preserved by a fairly general class of semantic constructors and which ones are reflected (conservativity). Moreover, we establish a correspondence between categories of computational models and categories of theories of the metalanguage, along the lines of Gabriel-Ulmer duality, in a type-theoretic framework. Using the Extended Calculus of Constructions, we develop a semantics for parallel composition by combining elementary notions of computation defined independently and we use LEGO to prove properties of such semantics formally.

It was the purpose of this design study to explore the Geometer’s Sketchpad dynamic mathematics software as a tool to model the derivative in introductory calculus in a manner that would foster a deeper conceptual understanding of the concept – developing domain specific understanding. Sketchpad’s transformation capabilities have been proved useful in the exploration of mathematical concepts by younger learners, college students and professors. The prospect of an open-ended exploration of mathematical concepts motivated the author to pursue the possibility of representing the concept of derivative in dynamic forms. Contemporary CAS studies have predominantly dwelt on static algebraic, graphical and numeric representations and the connections that students are expected to make between them. The dynamic features of Sketchpad and such like software, have not been elaborately examined in so far as they have the potential to bridge the gap between actions, processes and concepts on the one hand and between representations on the other. In this study Sketchpad model-eliciting activities were designed, piloted and revised before a final implementation phase with undergraduate non-math major science students enrolled for an introductory calculus course. Although most of these students had some pre-calculus and calculus background, their performance in the introductory course remained dismal and their grasp of the derivative slippery. The dual meaning of the derivative as the instantaneous rate of change and as the rate of change function was modeled in Sketchpad’s multiple representational capabilities. Six forms of representation were identified: static symbolic, static graphic, static numeric, dynamic graphic, dynamic numeric and occasionally dynamic symbolic. The activities enabled students to establish conceptual links between these representations. Students were able to switch systematically from one form of (foreground or background) representation to another leading to a unique qualitative understanding of the derivative as the invariant concept across the representations. Experimental students scored significantly higher in the posttest than in the pretest. However, in comparison with control group students the experimental students performed significantly better than control students in non-routine problems. A cyclical model of developing a deeper concept image of the derivative is therefore proposed in this study. / Educational Studies / D. Ed. (Education)