International Journal of Foundations of Computer Science

The purpose of this article is twofold. First, we show that Prolog's control constructs can be smoothly integrated into a functional language like Haskell. The resulting 'language', termed embedded Prolog, incorporates many of the features prescribed by the Prolog ISO standard: control constructs including the cut, all solution collecting functions, and error handling facilities. Embedded Prolog lacks some concepts such as logical variables but it inherits all of Haskell's strengths, eg static polymorphic typing, higher order functions etc. Technically, the integration is achieved using monads and monad transformers. One of the main innovations is the definition of a backtracking monad transformer, which allows us to combine backtracking with exception handling and interaction. Second, we work towards an axiomatization of the operations, through which the computational features are accessed. Equations are used to lay down the meaning of the various operations and their interrelations enabling the programmer to reason about programs in a simple calculational style. The axiomatization is applied to show that each finite computation has a simple canonical form.

An approach for systematically modifying the semantics of programming languages by semantics modifiers is described. Semantics modifiers are a class of programs that allow the development of general and reusable "semantics components". Language independence is achieved through the interpretive approach: an interpreter serves as a mediator between the new language and the language for which the non-standard semantics was implemented. Inverse computation, equivalence transformation and neighborhood analysis are shown to be semantics modifiers. Experiments with these modifiers show the computational feasibility of this approach. Seven modifier projections are given which allow the efficient implementation of non-standard interpreters and non-standard compilers by program specialization or other powerful program transformation methods.

It is observed that the proof of strong normalizability of typed terms of typed λ-calculus looks like the process of the model construction. The observation is clarified by the works of Hyland and Ong [8], Altenkirch [2], Stefanova and Geuvers [15], and so on. The model of Hyland and Ong is based on PL-category [14] and the model of Altenkirch or Stefanova and Geuvers is a non-categorical model that is specially designed for this purpose. In this paper, we will construct yet another categorical model for the second order λ-calculus — a non-extensional PL-category. To demonstrate the significance of the non-extensional model, we will give a model in which we can carry out the proof of the uniqueness of the β-normal form. The non-extensionality comes from the use of semi-adjoint for interpretation of abstraction and application (uncurry).