% Replace the following information with your document's actual % metadata. If you do not want to set a value for a certain parameter, % just omit it. % % Symbols permitted in metadata % ============================= % % Within the metadata, all printable ASCII characters except % '\', '{', '}', and '%' represent themselves. Also, all printable % Unicode characters from the basic multilingual plane (i.e., up to % code point U+FFFF) can be used directly with the UTF-8 encoding. % Consecutive whitespace characters are combined into a single % space. Whitespace after a macro such as \copyright, \backslash, or % \sep is ignored. Blank lines are not permitted. Moreover, the % following markup can be used: % % '\ ' - a literal space (for example after a macro) % \% - a literal '%' % \{ - a literal '{' % \} - a literal '}' % \backslash - a literal '\' % \copyright - the (c) copyright symbol % % The macro \sep is only permitted within \Author, \Keywords, and % \Org. It is used to separate multiple authors, keywords, etc. % % List of supported metadata fields % ================================= % % Here is a complete list of user-definable metadata fields currently % supported, and their meanings. More may be added in the future. % % General information: % % \Author - the document's human author. Separate multiple % authors with \sep. % \Title - the document's title. % \Keywords - list of keywords, separated with \sep. % \Subject - the abstract. % \Org - publishers. % % Copyright information: % % \Copyright - a copyright statement. % \CopyrightURL - location of a web page describing the owner % and/or rights statement for this document. % \Copyrighted - 'True' if the document is copyrighted, and % 'False' if it isn't. This is automatically set % to 'True' if either \Copyright or \CopyrightURL % is specified, but can be overridden. For % example, if the copyright statement is "Public % Domain", this should be set to 'False'. % % Publication information: % % \PublicationType - The type of publication. If defined, must be % one of book, catalog, feed, journal, magazine, % manual, newsletter, pamphlet. This is % automatically set to "journal" if \Journaltitle % is specified, but can be overridden. % \Journaltitle - The title of the journal in which the document % was published. % \Journalnumber - The ISSN for the publication in which the % document was published. % \Volume - Journal volume. % \Issue - Journal issue/number. % \Firstpage - First page number of the published version of % the document. % \Lastpage - Last page number of the published version of % the document. % \Doi - Digital Object Identifier (DOI) for the % document, without the leading "doi:". % \CoverDisplayDate - Date on the cover of the journal issue, as a % human-readable text string. % \CoverDate - Date on the cover of the journal issue, in a % format suitable for storing in a database field % with a 'date' data type. \Title {Functionality, polymorphism, and concurrency: a mathematical investigation of programming paradigms} \Author {Peter Selinger} \Copyright {Copyright \copyright\ 1997 Peter Selinger} \Keywords {lambda calculus\sep unorderability\sep polymorphism\sep PL-categories\sep Henkin models\sep communication processes\sep asynchronicity} \Subject {The search for mathematical models of computational phenomena often leads to problems that are of independent mathematical interest. Selected problems of this kind are investigated in this thesis. First, we study models of the untyped lambda calculus. Although many familiar models are constructed by order-theoretic methods, it is also known that there are some models of the lambda calculus that cannot be non-trivially ordered. We show that the standard open and closed term algebras are unorderable. We characterize the absolutely unorderable T-algebras in any algebraic variety T. Here an algebra is called absolutely unorderable if it cannot be embedded in an orderable algebra. We then introduce a notion of finite models for the lambda calculus, contrasting the known fact that models of the lambda calculus, in the traditional sense, are always non-recursive. Our finite models are based on Plotkin's syntactical models of reduction. We give a method for constructing such models, and some examples that show how finite models can yield useful information about terms. Next, we study models of typed lambda calculi. Models of the polymorphic lambda calculus can be divided into environment-style models, such as Bruce and Meyer's non-strict set-theoretic models, and categorical models, such as Seely's interpretation in PL-categories. Reynolds has shown that there are no set-theoretic strict models. Following a different approach, we investigate a notion of non-strict categorical models. These provide a uniform framework in which one can describe various classes of non-strict models, including set-theoretic models with or without empty types, and Kripke-style models. We show that completeness theorems correspond to categorical representation theorems, and we reprove a completeness result by Meyer et al. on set-theoretic models of the simply-typed lambda calculus with possibly empty types. Finally, we study properties of asynchronous communication in networks of communicating processes. We formalize several notions of asynchrony independently of any particular concurrent process paradigm. A process is asynchronous if its input and/or output is filtered through a communication medium, such as a buffer or a queue, possibly with feedback. We prove that the behavior of asynchronous processes can be equivalently characterized by first-order axioms.}