A formalism for the specification of essentially-algebraic structures in 2-categories

1992 ◽  
Vol 2 (1) ◽  
pp. 1-28 ◽  
Author(s):  
A. J. Power ◽  
Charles Wells
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
Two Dimensional ◽  
Functional Programming Languages ◽  
One Dimensional ◽  
Special Cases ◽  
Rewrite Rules ◽  
Definition Of

A type of higher-order two-dimensional sketch is defined which has models in suitable 2-categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of one-dimensional sketches. These sketches allow the specification of constructions in 2-categories such as weighted limits, as well as higher-order constructions such as exponential objects and subobject classifiers, that cannot be sketched by limits and colimits. These sketches are designed to be the basis of a category-based methodology for the description of functional programming languages, complete with rewrite rules giving the operational semantics, that is independent of the usual specification methods based on formal languages and symbolic logic. A definition of ‘path grammar’, generalizing the usual notion of grammar, is given as a step towards this goal.

Principal signatures for higher-order program modules

1994 ◽  
Vol 4 (3) ◽  
pp. 285-335 ◽  
Author(s):  
Mads Tofte
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Higher Order ◽  
Principal Type ◽  
Functional Programming Languages ◽  
Standard Ml ◽  
Static Semantics ◽  
Program Modules

AbstractIn this paper we present a language for programming with higher-order modules. The language HML is based on Standard ML in that it provides structures, signatures and functors. In HML, functors can be declared inside structures and specified inside signatures; this is not possible in Standard ML. We present an operational semantics for the static semantics of HML signature expressions, with particular emphasis on the handling of sharing. As a justification for the semantics, we prove a theorem about the existence of principal signatures. This result is closely related to the existence of principal type schemes for functional programming languages with polymorphism.

scholarly journals Dynamic game semantics

2020 ◽  
pp. 1-60
Author(s):  
Norihiro Yamada ◽  
Samson Abramsky
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Dynamic Game ◽  
Standard Interpretation ◽  
Functional Programming Languages ◽  
Game Semantics ◽  
Wide Range ◽  
Cartesian Closed Categories ◽  
Cartesian Closed

Abstract The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

What is a purely functional language?

1998 ◽  
Vol 8 (1) ◽  
pp. 1-22 ◽  
Author(s):  
AMR SABRY
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Denotational Semantics ◽  
Functional Language ◽  
Formal Definition ◽  
Functional Programming Languages ◽  
Precise Meaning ◽  
Definition Of ◽  
Parameter Passing

Functional programming languages are informally classified into pure and impure languages. The precise meaning of this distinction has been a matter of controversy. We therefore investigate a formal definition of purity. We begin by showing that some proposed definitions which rely on confluence, soundness of the beta axiom, preservation of pure observational equivalences and independence of the order of evaluation, do not withstand close scrutiny. We propose instead a definition based on parameter-passing independence. Intuitively, the definition implies that functions are pure mappings from arguments to results; the operational decision of how to pass the arguments is irrelevant. In the context of Haskell, our definition is consistent with the fact that the traditional call-by-name denotational semantics coincides with the traditional call-by-need implementation. Furthermore, our definition is compatible with the stream-based, continuation-based and monad-based integration of computational effects in Haskell. Finally, we observe that call-by-name reasoning principles are unsound in compilers for monadic Haskell.

On the λ Definable Higher Order Boolean Operations

1989 ◽  
Vol 12 (2) ◽  
pp. 181-189
Author(s):  
Marek Zaionc
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Higher Order ◽  
Truth Table ◽  
Boolean Operations ◽  
Functional Programming Languages

The purpose of this work is to show the methods of representing higher order boolean functionals in the simple typed λ calculus. In the paper is presented an algorithm for construction the λ representation of a functional given by generalized truth table. This technique is useful especially in functional programming languages such as ML in which functionals are expressed in the form of typed λ terms. Also λ representability of higher order functionals in many valued logics is discussed.

Uniqueness typing for functional languages with graph rewriting semantics

1996 ◽  
Vol 6 (6) ◽  
pp. 579-612 ◽  
Author(s):  
Erik Barendsen ◽  
Sjaak Smetsers
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Natural Deduction ◽  
Natural Extension ◽  
Type Systems ◽  
Higher Order ◽  
Functional Languages ◽  
Conventional System ◽  
Functional Programming Languages ◽  
Graph Rewriting

We present two type systems for term graph rewriting: conventional typing and (polymorphic) uniqueness typing. The latter is introduced as a natural extension of simple algebraic and higher-order uniqueness typing. The systems are given in natural deduction style using an inductive syntax of graph denotations with familiar constructs such as let and case.The conventional system resembles traditional Curry-style typing systems in functional programming languages. Uniqueness typing extends this with reference count information. In both type systems, typing is preserved during evaluation, and types can be determined effectively. Moreover, with respect to a graph rewriting semantics, both type systems turn out to be sound.

scholarly journals Higher-Order Logic Programming

1998 ◽  
Author(s):  
Gopalan Nadathur ◽  
Dale Miller
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Functional Programming ◽  
Ad Hoc ◽  
Order Type ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Functional Programming Languages ◽  
Logical Basis

Modern programming languages such as Lisp, Scheme and ML permit procedures to be encapsulated within data in such a way that they can subsequently be retrieved and used to guide computations. The languages that provide this kind of an ability are usually based on the functional programming paradigm, and the procedures that can be encapsulated in them correspond to functions. The objects that are encapsulated are, therefore, of higher-order type and so also are the functions that manipulate them. For this reason, these languages are said to allow for higher-order programming. This form of programming is popular among the users of these languages and its theory is well developed. The success of this style of encapsulation in functional programming makes is natural to ask if similar ideas can be supported within the logic programming setting. Noting that procedures are implemented by predicates in logic programming, higher-order programming in this setting would correspond to mechanisms for encapsulating predicate expressions within terms and for later retrieving and invoking such stored predicates. At least some devices supporting such an ability have been seen to be useful in practice. Attempts have therefore been made to integrate such features into Prolog (see, for example, [Warren, 1982]), and many existing implementations of Prolog provide for some aspects of higher-order programming. These attempts, however, are unsatisfactory in two respects. First, they have relied on the use of ad hoc mechanisms that are at variance with the declarative foundations of logic programming. Second, they have largely imported the notion of higher-order programming as it is understood within functional programming and have not examined a notion that is intrinsic to logic programming. In this chapter, we develop the idea of higher-order logic programming by utilizing a higher-order logic as the basis for computing. There are, of course, many choices for the higher-order logic that might be used in such a study. If the desire is only to emulate the higher-order features found in functional programming languages, it is possible to adopt a “minimalist” approach, i.e., to consider extending the logic of first-order Horn clauses— the logical basis of Prolog—in as small a way as possible to realize the additional functionality.

Operational aspects of untyped Normalisation by Evaluation

2004 ◽  
Vol 14 (4) ◽  
pp. 587-611 ◽  
Author(s):  
KLAUS AEHLIG ◽  
FELIX JOACHIMSKI
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Functional Programming Languages ◽  
Usual Type ◽  
Rewrite Rules ◽  
Operational Aspects

A purely syntactic and untyped variant of Normalisation by Evaluation for the $\lambda$-calculus is presented in the framework of a two-level $\lambda$-calculus with rewrite rules to model the inverse of the evaluation functional. Among its operational properties there is a standardisation theorem that formally establishes the adequacy of implementation in functional programming languages. An example implementation in Haskell is provided. The relation to the usual type-directed Normalisation by Evaluation is highlighted, using a short analysis of $\eta$-expansion that leads to a perspicuous strong normalisation and confluence proof for $\beta\eta\!\up$-reduction as a byproduct.

Sign in / Sign up

Export Citation Format

Share Document