Maarten M. Fokkinga

Weighted citation index

M.M. Fokkinga. Unregistered Technical Report, 2013, 7 pages.

Abstract. A citation index is one way of the many possibilities to measure "the quality'' of a researcher: count the citations to his work. The notion of citation index has many derived concepts, one of which is the h-index. In this note we consider one particular wish for a new definition of citation index of an author: when counting citations to the author's work, weigh (= multiply) each citation by the citation index of the citing author. We show how the weighted citation index can be computed in the MapReduce framework.

SQL versus coSQL -- a compendium to Erik Meijer's paper

M.M. Fokkinga. Unregistered Technical Report, 2001, 9 pages.

Abstract. In a seminal paper (A Co-Relational Model of Data for large Shared Data Banks, Comm. of the ACM, 54(4):49--58, April 2011), Erik Meijer enthusiastically shows an interesting relation between the well-known SQL and OO representations of facts from the real world. Phrased in terms of category theory, these turn out to be dualizations of each other (hence he speaks of SQL and coSQL), and many of their properties are in some sense dual to each other. This note enumerates most of his ideas in a quite different and more concise style, and might be used as a compendium to his paper.

Cost and feasibility estimations of an execution plan

M.M. Fokkinga. Unregistered Technical Report, 2010, 15 pages.

Abstract. The explanation by Kifer et al (in Database Systems: An Application-Oriented Approach, Complete Version, 2nd edition. Addison-Wesley, 2006) for calculating the total cost and amount of buffers of a query execution plan (is elegant, clear, well-phrased, correct, instructive and so on, but) does not take care of pipelining and the available buffers in a systematic way, and, instead, needs ad hoc reasoning for these aspects. We show a method that is systematic, easily to be automated, and needs no ad hoc reasoning when applied.

The Hough Transform

Maarten Fokkinga. Journal of Functional Programming (Functional Pearl), vol 21, issue 2, pp. 129-133, 2011, 5 pages.

Abstract. Suppose you are given a number of points in a plane and want to have those lines that each contain a large number of the given points. The Hough transform is a computerized procedure for that task. We show how the original procedure could have been derived. The derivation has the following notable properties: the crucial genuine idea falls out quite naturally in the course of our derivation, and we exploit the addition of functions.

Aggregation --- polymorphic and polytypic

M.M. Fokkinga. Unregistered Technical Report, 2011, 10 pages.

Abstract. Repeating the work of Meertens ``Calculate Polytypically!'' we show how to define in a few lines a very general ``aggregation'' function. Our intention is to give a self-contained exposition that is, compared to Meertens' work, more accessible for the uninitiated reader who wants to see the idea with a minimum of formal details.

Restricted Choices

M.M. Fokkinga. Unregistered Technical Report, 2011, 3 pages.

Abstract. Given are three numbers N,p,q with p at most 3N and q less than N. The problem is to determine the number of ways that one can choose p elements from a sequence of three sets of size N in such a way that in the first set more than p elements are chosen and in each of the second and third set at most q.

MapReduce formulation of PageRank

M.M. Fokkinga. Unregistered Technical Report, 2010, 4 pages.

Abstract. In a 12-line derivation we show how the (i+1)th approximation of the PageRank function can be calculated from the i-th approximation. The calculation is concise, machine checkable, and human readable at the same time. (We also provide the 3-page intuition that suggested this approach.)

Background info for Map and Reduce

M.M. Fokkinga. Unregistered Technical Report, 2009, 16 pages.

Abstract. What I will discuss falls in the range of Functional Programming up to Theory of Datatypes, and is meant to be background info for the MapReduce paradigm.

A Greedy Algorithm for Team Formation that is Fair over Time

M.M. Fokkinga. Unregistered Technical Report, 2009, 9 pages.

Abstract. In terms of a concrete example we derive a greedy algorithm for a hard problem. The problem is to compute a value which minimizes a given expression, and has exponential time complexity. The greedy algorithm computes a sub-optimal solution but has polynomial time complexity, and is fast enough for practical applications. The concrete problem is: the formation of teams from a given set of players such that, when repeated many times, each player is equally often teammate of each other player. The algorithm is easily coded in about thirty lines in a functional programming language. A few simple experiments give an indication of the quality of the greedy algorithm, and of some variants which trade quality for speed. We also abstract from the particulars of the concrete problem, and formalize our greedy algorithm in a general and abstract setting.

Word count --- the derivation

M.M. Fokkinga. Unregistered Technical Report, 2009, 6 pages.

Abstract. In a 2008 paper, Lämmel gives an elaborate discussion of the word count algorithm, resulting in an elaborate Haskell program taking 27 lines plus some libraries. He uses types to guide the construction of the word count algorithm as intended by Dean and Ghemawat in a 2004 paper. In contrast we use the word count specification to derive the intended word count algorithm. Another difference is that all our programs are "one-liners'', which makes it easy to manipulate them and do the derivation formally. We think that the short notations for maps and reduces are of great help to understand what's going on.

This is also part of another note.

MapReduce --- a two-page explanation for laymen

M.M. Fokkinga. Unregistered Technical Report, 2008, 2 pages.

Abstract. Map and Reduce are generic, useful notions for computing science; together they are equally expressive as simple inductive definitions over trees/lists/bags/sets.

Counting Join Trees

M.M. Fokkinga. Unregistered Technical Report, 2008, 2 pages.

Abstract. The number of non-equivalent ways to join n+1 different objects is n!(2n over n)/2^n.

Probabilistic Processing of Interval-valued Sensor Data

S. Evers and M. M. Fokkinga and P. M. G. Apers. In: Proceedings of the 5th International Workshop on Data Management for Sensor Networks (DMSN2008), Auckland, New Zealand, pp.42-48. ACM International Conference Proceeding Series, ACM. ISBN 978-1-60558-284-9, 2008, 7 pages.

Abstract. When dealing with sensors with different time resolutions, it is desirable to model a sensor reading as pertaining to a time interval rather than a unit of time. We introduce two variants on the Hidden Markov Model in which this is possible: a reading extends over an arbitrary number of hidden states. We derive inference algorithms for the models, and analyse their efficiency. For this, we introduce a new method: we start with an inefficient algorithm directly derived from the model, and visually optimize it using a sum-factor diagram.

The Right Expert at the Right Time and Place: From expertise identification to expertise selection

Pavel Serdyukov, Ling Feng, Arthur van Bunningen, Sander Evers, Harold van Heerde and Peter Apers, Maarten Fokkinga, Djoerd Hiemstra. In: Lecture Notes in Artificial Intelligence, volume 5345, Proceedings of the 7th International Conference on Practical Aspects of Knowledge Management (PAKM2008), Yokohama, Japan, pp.38--49, 2008, 12 pages.

Abstract. We propose a unified and complete solution for expert finding in organizations, including not only expertise identification, but also expertise selection functionality. The latter two include the use of implicit and explicit preferences of users on meeting each other, as well as localization and planning as important auxiliary processes. We also propose a solution for privacy protection, which is urgently required in view of the huge amount of privacy sensitive data involved. Various parts are elaborated elsewhere, and we look forward to a realization and usage of the proposed system as a whole.

Generative Modeling of Persons and Documents for Expert Search

P. Serdyukov and D. Hiemstra and M. M. Fokkinga and P. M. G. Apers. In: Proceedings of the 30th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval (SIGIR 2007), Amsterdam, Netherlands, pp. 827-828. ACM Press, ISBN 978-1-59593-597-7, 2007, 2 pages.

Abstract. In this paper we address the task of automatically finding an expert within the organization, known as the expert search problem. We present the theoretically-based probabilistic algorithm which models retrieved documents as mixtures of expert candidate language models. Experiments show that our approach outperforms existing theoretically sound solutions.

Composable Markov Building Blocks

S. Evers and M. M. Fokkinga and P. M. G. Apers. In: Proceedings of the 1st International Conference on Scalable Uncertainty Management (SUM 2007), Washington DC, USA. pp. 131-142. Lecture Notes in Computer Science 4772. Springer Verlag. ISBN 978-3-540-75407-7, 2007, 10 pages.

Abstract. In situations where disjunct parts of the same process are described by their own first-order Markov models and only one model applies at a time (activity in one model coincides with non-activity in the other models), these models can be joined together into one. Under certain conditions, nearly all the information to do this is already present in the component models, and the transition probabilities for the joint model can be derived in a purely analytic fashion. This composability provides a theoretical basis for building scalable and flexible models for sensor data.

Ranking Query Results using Context-Aware Preferences

A. H. van Bunningen and M. M. Fokkinga and P. M. G. Apers and L. Feng. In: First International Workshop on Ranking in Databases (DBRank 2007), April 16, 2007, Istanbul, Turkey. pp. 269-276. IEEE Computer Society Press. ISBN 978-1-4244-0832-0, 2007, 8 pages.

Abstract. To better serve users' information needs without requiring comprehensive queries from users, a simple yet effective technique is to explore the preferences of users. Since these preferences can differ for each context of the user, we introduce context-aware preferences. To anchor the semantics of context-aware preferences in a traditional probabilistic model of information retrieval, we present a semantics for context-aware preferences based on the history of the user. An advantage of this approach is that the inherent uncertainty of context information, due to the fact that context information is often acquired through sensors, can be easily integrated in the model. To demonstrate the feasibility of our approach and current bottlenecks we provide a naive implementation of our technique based on database views.

Exploring personalized life cycle policies

H. J. W. van Heerde and N. L. G. Anciaux and M. M. Fokkinga and P. M. G. Apers. Technical Report TR-CTIT-07-85, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625, 2007, 26 pages.

Abstract. Ambient Intelligence imposes many challenges in protecting people's privacy. Storing privacy-sensitive data permanently will inevitably result in privacy violations. Limited retention techniques might prove useful in order to limit the risks of unwanted and irreversible disclosure of privacy-sensitive data. To overcome the rigidness of simple limited retention policies, Life-Cycle policies more precisely describe when and how data could be first degraded and finally be destroyed. This allows users themselves to determine an adequate compromise between privacy and data retention. However, implementing and enforcing these policies is a difficult problem. Traditional databases are not designed or optimized for deleting data. In this report, we recall the formerly introduced life cycle policy model and the already developed techniques for handling a single collective policy for all data in a relational database management system. We identify the problems raised by loosening this single policy constraint and propose preliminary techniques for concurrently handling multiple policies in one data store. The main technical consequence for the storage structure is, that when allowing multiple policies, the degradation order of tuples will not always be equal to the insert order anymore. Apart from the technical aspects, we show that personalizing the policies introduces some inference breaches which have to be further investigated. To make such an investigation possible, we introduce a metric for privacy, which enables the possibility to compare the provided amount of privacy with the amount of privacy required by the policy.

An Answer Explanation Model for Probabilistic Database Queries

A. H. van Bunningen and L. Feng and M. M. Fokkinga and P. M. G. Apers. Technical Report TR-CTIT-07-41, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625, 2007, 20 pages.

Abstract. Following the availability of huge amounts of uncertain data, coming from diverse ranges of applications such as sensors, machine learning or mining approaches, information extraction and integration, etc. in recent years, we have seen a revival of interests in probabilistic databases. Queries over these databases result in probabilistic answers. As the process of arriving at these answers is based on the underlying stored uncertain data, we argue that from the standpoint of an end user, it is helpful for such a system to give an explanation on how it arrives at an answer and on which uncertainty assumptions the derived answer is based. In this way, the user with his/her own knowledge can decide how much confidence to place in this probabilistic answer. The aim of this paper is to design such an answer explanation model for probabilistic database queries. We report our design principles and show the methods to compute the answer explanations. One of the main contributions of our model is that it fills the gap between giving only the answer probability, and giving the full derivation. Furthermore, we show how to balance verifiability and influence of explanation components through the concept of verifiable views. The behavior of the model and its computational efficiency are demonstrated through an extensive performance study.

Associativity of Cartesian Product in Entity-Relation Diagrams

M.M. Fokkinga, Unregistered Technical Report, 2007, 1 page.

Abstract. Associativity of Cartesian product is well-known in set theory. The formulation of this folklore fact in terms of Entity-Relationship diagrams is less known (but equally true). We present the formulation and proof.

Possible Histories: A way to model Context-Aware Preferences

A. H. van Bunningen and M. M. Fokkinga. Technical Report TR-CTIT-06-78, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625, 2006, 11 pages.

Abstract. Nowadays more and more information becomes available in digital form. To be able to guide users through this wealth of information, a possibility is to only provide the user with relevant information, where relevancy is determined by the preferences of the user. To determine the precise relation between relevancy and preferences, we somehow need to formalize both concepts. This paper proposes a way to formalize the preferences of a user by grounding them in possible histories of the user. We explore this technique and its relations to other possible models.

Weak Entities Expressed Without Weakness

M.M. Fokkinga. Unregistered Technical Report, 2005, 3 pages.

Abstract. Weak entities can be described by Entity-Relationship diagrams without using the notion of weak entities.

Probabilistische Gegevensbanken --- een korte inleiding

M.M. Fokkinga, Unregistered Technical Report, 2005, 5 pages.

Abstract. Er zijn vele voorstellen gedaan voor het omgaan met onbepaaldheid in gegevensbanken. Een ervan is het idee van `probabilistische gegevensbanken'. Dat idee willen we hier duidelijk maken. Dat doen we door eerst van de klassieke gegevensbanken een voorbeeld te geven, dan aan de hand van dat zelfde voorbeeld probabilistische gegevensbanken te definieren, en tenslotte wat toepassingen (het nut ervan) te laten zien.

An explanation of forwards/backwards simulation

Maarten M. Fokkinga. Unregistered Technical Report, 2005, 3 pages.

Abstract. Forwards and backwards simulation are techniques to prove that a concrete program satisfies the specification that has been formulated in terms of an abstract program. There are cases where forwards simulation can be applied and not backwards simulation; the converse holds as well.

All this is probably folklore, but I've never seen so clear a presentation as the one that I now present myself...

Het ontwerpen van een databaseschema

Maarten M. Fokkinga. Unregistered Technical Report, 1st version 2005, 23 blz.

Abstract. In deze verhandeling geef ik een notatie en methode om een databaseschema te ontwerpen. Ik onderscheid in grote lijnen de volgende stappen: Beschrijf de werkelijkheid met een ER-diagram; Vertaal het ER-diagram naar een databaseschema door, zonder uitzondering, voor ieder entiteittype en iedere relatie een tabel te nemen; Normaliseer het databaseschema naar eerste normaalvorm; Optimaliseer het databaseschema; Normaliseer verder naar Boyce-Codd normaalvorm en 4e normaalvorm.

De databasearchitectuur van Panradio -- een zelflerende gedistribueerde muziekspeler

H.J.W. van Heerde, M.M. Fokkinga. Database Magazine DB/M, September 2005, vol.16, no.5, pp.41-44 (?), Array Publications b.v., Postbus 2211, 2400 CE Alphen aan den Rijn, Nederland, ISSN 0925-6911, 2005, 8 pages.

Abstract. Panradio is een systeem waarbij een gebruiker muziek voorgeschoteld krijgt die past bij zijn smaak. Het systeem is zelflerend, zodat het smaakprofiel van de gebruiker met het verloop van de tijd steeds beter wordt. Het systeem is gedistribueerd: de muziek wordt gehaald van de computers van alle gebruikers van Panradio.

Dit artikel beschrijft voornamelijk de architectuur, met bijzondere aandacht voor de systeemprestaties: het aantal gebruikers dat het systeem aan kan. Er wordt een model opgesteld dat de systeemprestaties beschrijft en kritische factoren aangeeft. Door uitgebreide tests zijn benaderingen van functies in het model gevonden, en optimalisaties geïdentificeerd.

Flattening Queries over Nested Data Models

J. van Ruth, M.M. Fokkinga, M. van Keulen. Unregisterd Technical Report, Submitted for publication, 2005, 10 pages.

Uitleg van de Hough transformatie

Maarten M. Fokkinga, Joeri van Ruth. Unregistered Technical Report, April 2005, 6 pages.

Abstract. De Hough transformatie is een wiskundige techniek om een stel figuren van gegeven vorm te vinden waarvan iedere figuur bij benadering gaat door veel gegeven punten. Wij zeten hier ons begrip van de techniek uiteen, zonder veel naar bestaand werk gekeken te hebben.

Constructing SQL queries

Maarten M. Fokkinga. Unregistered Technical Report, 2004 / 2005, 16 pages.

Abstract. SQL queries can be derived with 100% correctness from a natural language query by a calculation in set and predicate notation. This is particularly useful for queries involving quantifications hidden in the natural language formulation. The calculations lead not only to simple select-from-where formulations but also to formulations with a group-by and having clause. We recommend the approach in the teaching of SQL, observe the possibility of tools assistance, and call for future work to build tools that support the approach.

Ignorance in the Relational Model

Maarten M. Fokkinga. In: Proceedings of the 2nd Twente Data Management Workshop (TDM'06) on Uncertainty in Databases, 06 June 2006, Enschede. pp. 33-40. CTIT Workshop Proceedings Series (WP-CTIT-06-01). Centre for Telematics and Information Technology, University of Twente. ISSN 1381-3625, 2006, 8 pages.

Abstract. We hypothesize that an extension-with-conditioning of Dempster-Shafer theory is suitable for encoding uncertainty and ignorance in the Relational Model. We present a formal and well-motivated definition of conditioning, and show the spirit of the required change in the Relational Model and some results that then follow. It remains to be investigated whether these results are satisfactory.

The Dodo Query Flattening System

J. van Ruth, M.M. Fokkinga, M. van Keulen. Technical report, no.04-41, pp.1-51, Centre for Telematics and Information Technology (CTIT), University of Twente, ISSN 1381-3625, September 2004, 53 pages.

Abstract. Analytical query processing over complex objects often suffers from disappointing performance due to excessive use of nested-loop (element at a time) evaluation. Storing the data in a flattened form enables collection based processing (set at a time), gaining performance at the cost of having to write more complicated queries. This report proposes Dodo, an approach to automatic translation of queries from the complex objects domain into set-at-a-time operations against data stored in a flattened form.

Real-time location-based services for running races

S.P. Ekkebus, Maarten M. Fokkinga, Nirvana Meratnia. Submitted for publication, September 2004, 6 pages.

Abstract. This paper discusses the requirements and a basic system architecture for a real-time location-based service (LBS) for long-term speed running races. The envisioned system tracks the participating runners of the race and from this information spectators receive different types of services related to the race. The paper presents a design for a system, which combines GPS, cellular-network services and the Internet.

Extending the Relational Model with Uncertainty and Ignorance

Sunil Choenni, Henk Ernst Blok, Maarten Fokkinga. Technical report, no. TR-CTIT-04-29, Centre for Telematics and Information Technology, University of Twente, The Netherlands, ISSN 1381-3625, July 2004, 12 pages.

Abstract. It has been widely recognized that in many real-life database applications there is growing demand to model uncertainty and ignorance. However the relational model does not provide this possibility. Through the years a number of efforts has been devoted to the capture of uncertainty and ignorance in databases. Most of these efforts attempted to capture uncertainty using the classic probability theory. As a consequence, the limitations of probability theory are inherited by these approaches, such as the problem of information loss. In this paper, we extend the relational model with uncertainty and ignorance without these limitations posed by the other approaches. Our approach is based on the so-called theory of belief functions, which may be considered as a generalization of probability theory. Belief functions have an attractive mathematical underpinning and many intuitively appealing properties.

Formalization of Indexing in Databases

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, April 2004, 7 pages.

Abstract. Indexing is an important notion for efficient data management. It prescribes the use of a particular additional data structure for direct access to the locations where requested values have been stored. Indexing makes no assumptions about the organization and structure of the actual storage of values. All this is elegantly formalized in the Z notation.

"A Survey in Indexing and Searching XML Documents" in 337 one-liners

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, March 2004, 10 pages.

Abstract. This is my personal summary in 337 one-liners of "A Survey in Indexing and Searching XML Documents" by Luk et al. (2002). I focus on technical aspects, omitting all system names and references.

FDFD: Formal Derivations of Functional Dependencies

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Netherlands, February 2004, 7 pages.

Abstract. We show that, and how, functional dependencies can be formally derived from a case description in natural language.

Z-style notation for Probabilities

Maarten M. Fokkinga. In: Proceedings of the 2nd Twente Data Management Workshop (TDM'06) on Uncertainty in Databases,, Enschede. pp. 19-24. CTIT Workshop Proceedings Series (WP-CTIT-06-01). Centre for Telematics and Information Technology, University of Twente. ISSN 1574-0846, June 2006, 6 pages.

Abstract. A notation for probabilities is proposed that differs from the traditional, conventional notation by making explicit the domains and bound variables involved. The notation borrows from the Z notation, and lends itself well to calculational manipulations, with a smooth transition back and forth to set and predicate notation.

Aligning Application Architecture to the Business Context

R.J. Wieringa, H.M. Blanken, M.M. Fokkinga, P.W.P.J. Grefen. In: Johann Eder, Michelle Missikoff / Advanced Information System Engineering / vol.2681 / Lecture Notes in Computer Science / Springer-Verlag / ISBN 3-540-40442-2 / Proceedings, 15th International Conference on Advanced Information System Engineering, CAiSE 2003, held in Klagenfurt, Austria, June 16-18, 2003, pp.209-225, 2003, 17 pages.

Abstract. Alignment of application architecture to business architec- ture is a central problem in the design, acquisition and implementation of information systems in current large-scale information-processing organi- zations. Current research in architecture alignment is either too strategic or too software implementation-oriented to be of use to the practicing information systems architect. This paper presents a framework to an- alyze the alignment problem and operationalizes this as an approach to application architecture design given a business context. We summarize guidelines for application architecture design and illustrate our approach and guidelines with an example.

Construction of SQL group-by queries

Maarten M. Fokkinga. Unregistered Technical Note, August 2003.

Please, see the successor paper: "Constructing SQL queries (2004)".

Abstract. We set out to find the set and predicate notation corresponding to SQLs group-by clause, and find useful rules for manipulation those notations so as to be able to calculate a SQL group-by query from an initial set notation of the query.

XML notions formalized

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, April 2003, 18 pages.

Abstract. We provide a formal definition of several XML notions: schema, document, validity (of a document for a schema), query and answer, and integration. The definitions have the following properties:

• precise and intuitive at the same time,

• using common, standard mathematical notions wherever possible,

• at a high level of abstraction (= many aspects are not dealt with),

• suitable for use in proving properties.

(Admittedly, being intuitive is a rather subjective property, and the suitability for proving properties has to be established yet.) This work arose in attempt to understand some definitions in an early working version of Marko's paper ``XML schema integration --- the Xblock approach''.

About XML integration and distribution

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, April 2003, 2 pages.

Abstract. We attempt to characterize the goals that we have in mind when formalizing the relation between distributed XML query processing and integration.

Sequence comprehension for XQuery's FLWOR expression

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 2003, 2 pages.

Abstract. In XQuery the FLWOR expression is a kind of comprehension for sequences. It differs from sequence comprehensions as found in functional programming languages mainly in the presence of an order by clause. We define a sequence expression with an order by clause that is suitable to express the semantics of XQuery's FLWOR expressions.

Comparing Refinements for Failure and Bisimulation Semantics

R. Eshuis, M.M. Fokkinga. Fundamenta Informaticae, vol.52, no.4, pp.297-321, 2002, 25 pages.

Abstract. Refinement in bisimulation semantics is defined differently from refinement in failure semantics: in bisimulation semantics refinement is based on simulations between labelled transition systems, whereas in failure semantics refinement is based on inclusions between failure systems. There exist however pairs of refinements, for bisimulation and failure semantics respectively, that have almost the same properties. Furthermore, each refinement in bisimulation semantics implies its counterpart in failure semantics, and conversely each refinement in failure semantics implies its counterpart in bisimulation semantics defined on the canonical form of the compared processes.

Keywords: refinement, labelled transition systems, bisimulation semantics, failure semantics, decorated traces.

Data exchange over web-based applications

Roelof van Zwol, M.M. Fokkinga, V. Jeronimus, Peter M.G. Apers. In: Zo Lacroix / Proceedings 2nd International Workshop on Data Integration on the Web, DIWeb'02 / University of Toronto Press / Toronto, Canada, pp. 17-33, 2002, 22 pages.

Abstract. With large volumes of data being exchanged on the Internet, query languages are needed to bridge the gap between databases and the web. Furthermore, the differentiation in data types used by web- based applications is ever growing, despite all standardization efforts. The Data eXchange Language (DXL) provides an extensible base language designed to exchange data from heterogeneous sources into a single target.

One application of DXL, the focus in this article, is to retrieve data from databases, and yield the result in an XML document. However, the real application area of DXL is much broader since DXL provides a framework which allows data of a particular source to be queried and/or constructed by its original query language. This is achieved by DXL's extensibility mechanism which allows other query languages to be embedded into a DXL query.

Ternaire relaties in ERDs zijn lastig

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, June 2002, 7 pages.

Abstract. In het afgelopen tentamen OIS (Ontwerpen van Informatiesystemen; 233026) stond onderstaande opgave over ER-modelering. Geen enkele van de twintig studenten had een volledig correcte uitwerking. Maar ook geen enkele van mijn collega's! Ook ikzelf niet. En zelfs de oplossing in het boek Design Methods for Reactive Systems is niet 100% correct. Iedereen heeft natuurlijk wel iets goed; maar ja, wat heb je aan een specificatie die fout is? Ik geef de opgave zoals die (op een kleine correctie na) op het tentamen gesteld is. Ik daag de lezer uit eerst zelf een tot in details uitgewerkte oplossing te bedenken (en bijhorende argumentatie te geven) en alternatieven te beschouwen, alvorens naar het antwoord te kijken. Je zult versteld staan van de valkuilen die zich bij deze ER-modellering voordoen.

The associativity of equivalence and the Towers of Hanoi problem

R.C. Backhouse, M.M. Fokkinga. Information Processing Letters, vol.77, no.2-4, pp.71-76, 2001, 6 pages.

Abstract. Dijkstra and Scholten have argued that greater use should be made of the associativity of equivalence. This note shows how the property is used in specifying the rotation of the disks in the well-known Towers of Hanoi problem.

A Process Model for Life Cycles

Maarten M. Fokkinga, Rick van Rein. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 2001, 15 pages.

Abstract. Life cycles (discussed elsewhere regarding the informal and pragmatic aspects) can be formally defined as a process model with some un-conventional features, namely: multiplicity of events, a restricted visibility of parameters, and `negative prefixes' to block an event set from happening. We show how to translate these aspects in terms of conventional process constructs.

Several times we manage to present the proofs of an implication and its converse that use different induction hypotheses as one series of equivalences.

This presentation technique seems more generally applicable to and useful for process models.

DXL: Data eXchange Language

R. van Zwol, V.Jeronimus, M.M. Fokkinga, P.M.G. Apers. Technical report, no. TR-CTIT-01-47, University of Twente, Centre for Telematics and Information Technology (CTIT), PO Box 217, NL 7500 AE Enschede, ISSN 1381-3625, December 2001, 17 pages.

Abstract. With large volumes of data being exchanged over the Internet query languages are needed to bridge the gap between databases and the web. DXL provides an extendible framework, designed to exchange data between heterogeneous sources and targets, such as databases and XML documents. One application of DXL, the focus in this article, is to retrieve data from databases and yield the result in XML documents. The major contribution of DXL compared to other query languages, like RXL and XQuery, is that the structure of an output XML document may depend not only on the DXL query but also on the source data. To achieve this DXL uses a construct clause, where the structure of the XML document is (partially) defined, but unlike other XML query languages this clause is embedded in a template, which can be called recursively. We demonstrate the power of DXL with a newsgroup example, where each posted message may have arbitrarily nested follow-ups. The extendibility of the framework is ensured by using XML to describe the syntax of DXL. Besides discussing the syntax, semantics, and the newsgroup application of DXL, we will also show how heterogeneous sources can be queried and integrated into a single XML document, and we discuss the architecture that is setup to implement DXL.

Documenting the ICT Architecture of TSI

R.J. Wieringa, H.M. Blanken, M.M. Fokkinga. Technical report, no. TR 01-42, University of Twente, Centre for Telematics and Information Technology (CTIT), PO Box 217, NL 7500 AE Enschede, ISSN 1381-3625, December 2001, 25 pages.

Abstract. We use the business and software architecture of Travel Service International (TSI) as a case study to validate our approach to ICT architecture. The techniques discussed are explained at length in a textbook by Wieringa.

An alternative approach to I/O

Maarten M. Fokkinga, Jan Kuper. Technical report, no. TRCTIT-01-44, pp.1-12, University of Twente, Centre for Telematics and Information Technology (CTIT), Enschede, Netherlands, ISSN1381-3625, December 2001, 12 pages.

Abstract. We propose a form of input and output for functional languages that is in a sense orthogonal to the actual computation: certain input and output directives can be added to a completed, fully working program text, and they do neither disturb referential transparency nor necessitate to change the types of the program text. The input and output directives change the order of evaluation as little as possible (lazy evaluation remains lazy), though there is sufficient control over the order in which the input and output actions occur to make it acceptable for the user. The basic idea is that a value which is written out explicitly in the program text by way of typical example, is replaced by a special constant that asks the user to type in parts of the value, as needed by the computation. The mechanism seems suitable for a large class of so-called interactive programs.

Formal semantics of ERDs

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, September 2001, 6 pages.

Abstract. The principal interpretation of an ERD (Entity-Relationship Diagram) consists of individuals, concepts, and properties in the real world; the interpretation is inherently informal and subjective! Nevertheless, the notation also has an interpretation of its own, in abstract mathematical terms rather than concrete real world terms. The existence of such an interpretation is important, because it enables us to decide various questions about the notation without resorting to informal (hence subjective) arguments.

In this note we give a "translation'' of an ERD to its formal semantics. It will turn out that the formal semantics takes a lot more symbols and piece of paper than the ERD itself. This indicates that ERDs are a concise notation; giving only the mathematical formulas instead of a graphical ERD would be unpractical. The mathematical semantics comes into play only to give rigorous proofs of theorems about ERDs (such as verifications of checking and manipulations by tools!), or to explain dark corners of the principal interpretation of ERDs.

Towards a Theory of Moa

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, September 2000, 12 pages.

Abstract. This note proposes an approach to a "Theory of MOA'' --- the completion of which is deemed worth (and proposed as) a full PhD thesis. The objective of the theory is threefold: first it should provide `insight' in the principles of MOA (possibly leading to improvements in the documentation, explanations, and so on), second it should provide a formal framework to formulate and prove various claims and properties of MOA, and third it should suggest generalisations (possibly leading to an improved or more general system). In order to achieve the right level of abstraction and generality, we will use some methods and notions from category theory; using category theory is not an aim in itself.

@techreport{db-utwente:tech:0000003550, author = {Fokkinga, Maarten M.}, title = {{Towards a Theory of Moa}}, month = sep, year = {2000}, pages = {1--12}, institution = {University of Twente}, address = {Enschede, Netherlands}, note = {Unregistered Technical Report} } % private key: \mmfkey{mmf2000b}

On the Iterative Solution of the Towers of Hanoi Problem

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, May 2000, 4 pages.

Abstract. We give an elegant proof (formal, calculational, readable, machine verifiable, without case distinctions) of the property that in the Towers of Hanoi solution all disks cycle.

View integration

Herman Balsters, Maarten Fokkinga, Maurice van Keulen. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 1999, 4 pages.

Abstract. Suppose that we are to build one information system (database, say) for several users that each have their own view of the world. The idea is to integrate the views of all individual users into one view (which is satisfactory for all users), and build the information system for that view. The problem that we are faced with is this: What is the/a formal definition of view integration that serves this purpose? We tackle this question, dealing with integration on the schema level as wel as on the world/extension level, and we will make explicit various assumptions. It remains to be investigated whether our notion of view integration (with the motivation above) is also suitable for federated databases and datawharehousing.

Comparing Refinements for Failure and Bisimulation Semantics

R. Eshuis, M.M. Fokkinga. In: WAIT99 Workshop Argentino de Informatica Teorica / Sociedad Argentina de Informatica e Investigacion / Uruguay 252 2 D, (1015) Buenos Aires, Argentina, September 1999, pp.65-80, 16 pages.

Abstract. Refinement in bisimulation semantics is defined differently from refinement in failure semantics: in bisimulation semantics refinement is based on simulations between labelled transition systems, whereas in failure semantics refinement is based on inclusions between decorated traces systems. There exist however pairs of refinements, for bisimulation and failure semantics respectively, that have almost the same properties. Furthermore, each refinement in bisimulation semantics implies its counterpart in failure semantics, and conversely each refinement in failure semantics implies its counterpart in bisimulation semantics defined on the canonical form of the compared processes.

Keywords: refinement, decorated traces, labelled transition systems, bisimulation semantics, failure semantics.

Protocol Assuring Universal Language

R. van Rein, M.M. Fokkinga. In: P. Ciancarinia, A. Fantechi, R. Gorrieri / Formal Methods for Open Object-Based Distributed Systems, Florence, Italy / Kluwer Academic Publishers / ISBN 0-7923-8429-6 / Proceedings International Conference, Florence, Italy, pp.241-258, February 1999, 18 pages.

Abstract. Conventionally, interfaces of objects export a set of messages with their types, and suggest nothing about the order in which these services may be accessed. This leaves room for a large number of run-time errors or misbehaviours in type correct designs. To mend this, we introduce the notion of protocol, expressing offered and expected orderings of messages, along with a notion of protocol correctness. We do this by defining the Protocol Assuring Universal Language Paul, which describes protocol aspects of classes, and serves as a basis for formal study.

Keywords: object orientation, interface, behaviour, role, protocol, process, type checking, Paul.

Expressions that talk about themselves

Maarten M. Fokkinga. The Computer Journal, no.5, pp.408-412, 1996, 5 pages.

Abstract. Self-reference occurs frequently in theoretical investigations of formal systems. In Predicate Logic self-reference is used in G\"odels Incompleteness Theorem: a formula is constructed that asserts ``I am not formally provable''; in a programming language self-reference manifests itself in the existence of a program that writes its own text, a so-called self-reproducing program. Also in Nature self-reference plays a role, in the ability of self-reproduction of the formal system of DNA molecules. Odifreddi~\cite[page 165--174]{odifreddi89} discusses these topics and gives good references to the literature.

In this note we explain, independent of any formalism, how to construct an expression in a formal system that ``does something with itself''. As an application of this procedure we show how to construct a program that writes its own text, lay-out included. (Our self-reproducing Miranda script is, after some optimisation, exactly 36 characters long!)

De WeetNiet-WistAl-WeetWel-WeetOok puzzel

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 1996, 4 pages.

Abstract. Aan twee personen zijn het product en de som van twee verschillende positieve gehele getallen onder de honderd gegeven. Op de vraag wat die getallen zijn, zeggen zij achtereenvolgens en om beurten: "Ik weet het niet'', "Dat wist ik al'', "Nu weet ik het wel'', "Nu weet ik het ook''. Wij construeren een elegant programma dat het getallenpaar oplevert.

DHZ-3D

M.M. Fokkinga and Jan Kuper. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 1996, 15 pages.

Abstract. 3D plaatjes (plaatjes waarop een afbeelding in drie dimensies gezien kan worden) hebben een heel regelmatige structuur. We construeren een eenvoudig programma waarmee gemakkelijk DoeHetZelf 3D plaatjes gemaakt kunnen worden.

Magische woordvierkanten

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 1996, 3 pages.

Abstract. Gegeven is een lijst van woorden. Gevraagd wordt alle mogelijke 4x4-vierkanten van letters waarin elke rij en elke kolom een woord is uit een gegeven woordenlijst. Hiervoor wordt een Miranda-programma ontwikkeld.

Flippos --- de nieuwe rage

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, April 1996, 18 pages.

Abstract. In iedere zak chips (van het juiste merk) zitten een of meer flippos: kleine ronde kunststof schijfjes. Je kunt ermee bouwen (de techno-flippos), gooien (de gewone flippos), ruilen of gewoon sparen (hoe meer hoe beter, vindt de chips-fabrikant). Op sommige staat zelfs een puzzel; en daar gaat hier over. Op zo'n puzzel-flippo staan vier cijfers waarmee je een sommetje moet construeren met 24 als uitkomst; elk cijfer moet precies eenmaal in het sommetje voorkomen (als getal), en de bewerkingen *, /, +, - mogen daarbij worden gebruikt. Bijvoorbeeld, met de cijfers 1,4,7,7 kunnen we het sommetje (1+7)*(7-4) maken met 24 als uitkomst.

Wij zullen nu een Miranda script maken waarmee flippo-puzzels zijn op te lossen en te genereren. Er is ruimte genoeg om mee te denken: er zijn 26 opgaven met antwoorden.

Machine Assisted Constraint Maintenance

Maarten M. Fokkinga. Unregistered technical report, University of Twente, Enschede, Netherlands, October 1996, 3 pages.

Abstract. Constraints in databases may be maintained while transactions are executed, by the automatic invocation of suitable rules containing actions that compensate any constraint violation within the transactions. There is ample opportunity for machine assistence in the construction of the rules. The correctness and termination of a collection of rules follows from local correctness and termination properties for the individual rules, which are left to the responsibility of the user.

This is a summary of the 1990 paper by Ceri and Widom, rephrased on a very abstract level and provided with alternative and simpler proofs.

OO versus FP --- a little case study

M.M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, 1995, 10 pages.

Abstract. We describe what we think is the essence of Object-Orientedness (OO), and then show by means of an example how this style translates into a Functional Programming (FP) notation. The example is the case of two thermometers, with possibly different scales (Centigrades, Fahrenheit, or whatever), that can be used separately but also in a coupling in such a way that the coupled pair behaves consistently.

Program Specifications for Program Simulations

M.M. Fokkinga, J.C.S.P. van der Woude, J. Zwiers. Unregistered Technical Report, University of Twente, Enschede, Netherlands, February 1995, 8 pages.

Abstract. We give a concise, structured, and calculational proof of a theorem that yields a program specification for a given, specific, program simulation.

Keywords: program correctness, programming calculi.

Notities bij `Informatiesystemen'

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, November 1994, 19 blz.

Abstract. Deze bundel bevat een aantal notities die ik in de loop van het trimester gemaakt heb naar aanleiding van mijn overpeinzingen bij het vak Informatiesystemen.

Constructie van contextdiagrammen

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, September 1994.

Co-algebras --- a short summary

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, September 1994, 6 pages.

Abstract. Co-algebras are dual to algebras, and finality is dual to initiality. We shall be very brief in the formal exposition, since it is just a matter of dualisation, but more elaborate in the informal explanation and examples.

A Summary of Refinement Theory

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, September 1994, 12 pages.

Abstract. When can a program part be replaced by another? We discuss this question formally, and in doing so we summarize the work of Zwiers et al. ("A Note on Compositional Refinement'' and some private communication) and part of the work of Hoare et al. ("The weakest prespecification'' and "Prespecification in data refinement'').

Monadic Maps and Folds for Arbitrary Datatypes

Maarten M. Fokkinga. Technical report, no. Memoranda Inf 94-28, University of Twente, Enschede, Netherlands, June 1994, 23 pages.

Abstract. Each datatype constructor comes equiped not only with a so-called map and fold (catamorphism), as is widely known, but, under some condition, also with a kind of map and fold that are related to an arbitrary given monad.

This result follows from the preservation of initiality under lifting from the category of algebras in a given category to a certain other category of algebras in the Kleisli category related to the monad.

Dyads, a generalisation of monads

Maarten M. Fokkinga. Technical report, no. Memoranda Inf 94-30, University of Twente, Enschede, Netherlands, ISSN 0924-3755, June 1994, 8 pages.

Abstract. The concept of dyad is defined as the least common generalisation of monads and co-monads. So, taking some of the ingredients to be the identity, the concept specialises to the concept of monad, and taking other ingredients to be the identity it specialises to co-monads. Except for one axiom, all have a nice ("natural'') form.

Abstracte Datatypen en Categorie-Theorie

Maarten M. Fokkinga. Technical report, no. Memoranda Inf 94-32, University of Twente, Enschede, Netherlands, ISSN 0924-3755, June 1994, 23 pages.

Abstract. Sommige datatypen kunnen volledig met axioma's gekarakteriseerd worden, zonder op enigerlei wijze voor te schrijven hoe de elementen van het datatype er uit zien; we spreken dan van abstract datatype. We laten de karakterisering en enige stellingen en bewijzen in detail zien voor het cartesisch product en disjoint union van twee verzamelingen.

De begrippen en methoden die een rol spelen komen uit de categorie-theorie.

Tail invariants

Maarten M. Fokkinga. Unregistered Technical Note, University of Twente, Enschede, Netherlands, June 1994, 4 pages.

Abstract. Tail invariants are weaker than normal invariants, and thus allow for more program manipulations. This is shown formally in a very general setting.

Modular Completeness for Communication Closed Layers

Maarten M. Fokkinga, Mannes Poel, Job Zwiers. In: Eike Best / Proceedings CONCUR '93 / vol.715 / Lecture Notes in Computer Science / Springer-Verlag / ISBN 3-540-57208-2, pp.50-65, August 1993, 16 pages.

Abstract. The Communication Closed Layers law is shown to be modular complete for a model related to that of Mazurkiewicz. It is shown that in a modular style of program development the CCL rule cannot be derived from simpler ones. Within a non-modular set-up the CCL rule can be derived however from a simpler independence rule and an analog of the expansion rule for process algebras.

State-based functional frogramming

Maarten M. Fokkinga. Unregistered Technical Report, University of Twente, Enschede, Netherlands, July 1993, 9 pages.

Abstract. The usual "map f'' is adapted so as to accept and produce a state value that is single-threaded through the computation. This is an elaboration of Section 4 (3 pages; not including 4.1) of the paper "Type parametric programming with compile-time reflection'' by Tim Sheard.

Calculate categorically!

M.M. Fokkinga. Formal Aspects of Computing, vol.4, no.4, pp.673-692, Springer-Verlag, ISSN 0934-5043, 1992, 23 pages.

Abstract. Diagram chasing is an established proof technique in Category Theory. Algebraic calculation is a good alternative; made possible thanks to a notation for various unique arrows and a suitable formulation of initiality, and the calculational properties brought forward by initiality.

Law and order in Algorithmics

Maarten M. Fokkinga. Introduction to the Doctoral Dissertation of the same title, in Dutch; appeared in I/O-Vivat, December 1992, 10 pages.

Abstract. Algoritmiek (engels: algorithmics) is de theorie en praktijk van het algebraisch redeneren over programma's. Een elementaire stap in een algebraische redenering over programma's wordt wet genoemd (engels: law). Het systematisch ontdekken en gebruiken van wetten voor programma's is het onderwerp van mijn promotie-onderzoek geweest. Dit verhaal geeft een overzicht van dat onderzoek.

Lecture Notes of the STOP 1992 Summerschool on Constructive Algorithmics

Maarten Fokkinga, Johan Jeuring. vol. Part I, University of Utrecht, Utrecht, Netherlands, September 1992.

Categorical construction of the induced congruence

M.M. Fokkinga. Unregistered Technical Report, CWI, Amsterdam, 1991, 9 pages.

Abstract. Given an algebra and a relation on its carrier, we construct categorically the least equivalence relation containing the relation and being a congruence for (the operations of) the algebra. We need to assume that the base category is omega-cocomplete, and has all finite coequalisers, pushouts, and kernel pairs (pullbacks of equal pairs); the functor of the algebra has to be omega-cocontinuous. Note (added in proof): there is still a "small'' gap in the correctness proof: the omega-cocontinuity of the so-called Kernel pair functor is not yet clear.

Subtyping can have a Simple Semantics

H. Balsters, M.M. Fokkinga. Theoretical Computer Science, vol.87, pp.81-96, Elsevier, 1991, 15 pages.

Abstract. Consider a first order typed language, with semantics S for expressions and types. Adding subtyping means that a partial order < on types is defined and that the typing rules are extended to the effect that expression e has type t whenever e has type s and s<t. We show how to adapt the semantics S in a simple set theoretic way, obtaining a semantics S' that satisfies, in addition to some obvious requirements, also the property that: S' s is included in S' t, whenever s<t.

An exercise in transformational programming: Backtracking and Branch-and-Bound

Maarten M. Fokkinga. Science of Computer Programming, vol.16, no.1, pp.19-48, Elsevier, North-Holland, Amsterdam, The Netherlands, ISSN 0167-6423, July 1991, 26 pages.

Abstract. We present a formal derivation of program schemes that are usually called Backtracking programs and Branch-and-Bound programs. The derivation consists of a series of transformation steps, specifically algebraic manipulations, on the initial specification until the desired programs are obtained. The well-known notions of linear recursion and tail recursion are extended, for structures, to elementwise linear recursion and elementwise tail recursion; and a transformation between them is derived too.

Initial Many-sorted Algebras

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, 1991, 5 pages.

Abstract. An initial mny-sorted algebra can be expressed (constructed) as a collection of many single-sorted algebras.

Calculation Properties of Initiality

Maarten M. Fokkinga. Unregisterd technical report, CWI, Amsterdam, April 1991, 17 pages.

Abstract. We give a systematic treatment of the calculation properties brought forward by initiality, and finality.

Map-functor factorized

M.M. Fokkinga, L. Meertens. The Squiggollist, Vol 2, Nr 1, pages 17-19, March 1991, 3 pages.

Abstract. It is well known that any initial data type comes equipped with a so-called map-functor. We show that any such map-functor is the composition of two functors, one of which is —closely related to— the data type functor, and the other is —closely related to— the function µ (that for any functor F yields an initial F -algebra, if it exists).

A Translation from Attribute Grammars to Catamorphisms

Maarten M. Fokkinga, J.T. Jeuring, L. Meertens, E. Meijer. The Squigollist, Vol 2, Nr 1, pages 20--26, March 1991, 7 pages.

Abstract. Let AG be an attribute grammar, with underlying context free grammar G and attribute evaluation rules A . The function that decorates —according to A— a parse tree with attribute values and then delivers the synthesized attribute value of the root node, is denoted [[A]] . We translate G into a functor F such that any parse tree for G is an element of the initial F -algebra. The attribute evaluation rules A are translated to a function ϕ such that ([F | ϕ]) is, in a precise sense, equivalent to [[A]] .

Prepromorphisms

Maarten M. Fokkinga. Unregistered Technical Report, CWI, Amsterdam, March 1991, 8 pages.

Abstract. We study a recursion scheme that differs from the scheme for catamorphisms in that the recursive calls are preceded by some preprocessing. We give sufficient conditions under which such a scheme has a unique solution. The solution, if it exists, is termed a prepromorphism. An important prepromorphism is the so-called f-cascade. Of course, dualisation applies here; it provides the solution to the problem of proving the equivalence of two ways of de defining f-iterate. The proof technique may be of greater importance than the particular theorem for which it is used here; it uses in infinite tuplings of morphisms.

The Category of Categories is Cartesian Closed

Maarten M. Fokkinga. Unregistered Technical Report, CWI, Amsterdam, February 1991, 3 pages.

Abstract. The category of categories is cartesian closed. This means amongst others that curry(†) is well defined for any bi-functor † , having the properties that we expect it to have. The sectioning notation x† may be used to denote “ x subject to curry(†) ” (for object or morphism x ); it follows that f† is a natural transformation from A† to B† , whenever f : A → B.

Program Calculation Properties of Continuous Algebras

M.M. Fokkinga, E. Meijer. Technical report, no. CS-R9104, CWI, Amsterdam, Netherlands, January 1991, 47 pages.

Abstract. Defining data types as initial algebras, or dually as final co-algebras, is beneficial, if not indispensible, for an algebraic calculus for program construction, in view of the nice equational properties that then become available. It is not hard to render finite lists as an initial algebra and, dually, infinite lists as a final co-algebra. However, this would mean that there are two distinct data types for lists, and then a program that is applicable to both finite and infinite lists is not possible, and arbitrary recursive definitions are not allowed. We prove the existence of algebras that are both initial in one category of algebras and final in the closely related category of co-algebras, and for which arbitrary (continuous) fixed point definitions (“recursion”) do have a solution. Thus there is a single data type that comprises both the finite and the infinite lists. The price to be paid, however, is that partiality (of functions and values) is unavoidable.

We derive, for any such data type, various laws that are useful for an algebraic calculus of programs.

CR categories and descriptors: D11 [Software]: Programming Techniques — Applicative Programming, D31 [Software]: Programming Languages — Semantics, F32 [Theory of Computation]: Logic and meanings of Programs — Algebraic approach to semantics, F33 [Theory of Computation]: Logic and meaning of programs — type structure.

General terms: algorithm, design, theory.

Additional keywords and phrases: algebraic calculus for program construction, data type, algebra, complete partial ordered set (cpo), recursion, initiality, finality, anamorphism, catamorphism.

Exploiting Associativity

M.M. Fokkinga. In: Liber Amicorum at the occasion of Lambert Meertens 25th CWI anniversary, pp.24-28,1990, 4 pages.

Abstract. It is well-known that for the standard implementation of cons-lists, as in Miranda and Lisp, the reduction to canonical form of x ++ y takes size x steps, given that x and y are in canonical form. This is because the catenate operation ++ for cons-list is defined by induction on the structure of its left argument as a repeated cons. So, although (x ++ y) ++ z = x ++ (y ++ z), reduction of the left-hand side takes size x + size (x ++ y) = 2 times size x + size y steps, but only size x + size y steps for the right-hand side. It is therefore more efficient to compute the value of an expression x1 ++ x2 ++ ... ++ xn (with some parenthezation) by evaluating x1 ++ ( x2 ++ ( ... ++ xn)) instead (with the parentheses grouped to the right). Less than four years ago I gave a formal treatment of this phenomenom in a seven page note (``Elimination of Left-nesting: an example of the style of functional programming''). Nowadays, in the current status of Constructive Algorithmics and Squiggol Notation, developed by Lambert Meertens and others, it is hardly more than a simple exam question. As a show of what I have learned from Lambert ---and maybe of what I still have to learn--- I will discuss a generalisation of the elimination of left-nesting in full.

Adjunctions formulated as cata/anamorphisms

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, December 1990, 4 pages.

Abstract. This exposition is nothing but a formulation of the notion of adjunction in a terminology that is close to our current conventions in Constructive Algorithmics. It has been proposed by Lambert Meertens.

Sum, Product and Exponent defined as Cata/anamorphisms

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, November 1990, 4 pages.

Abstract. It is shown that the categorical sum, with associated morphisms, may be defined as an initial algebra, with associated catamorphisms and maps; and dually for product, final algebra, and anamorphisms. This holds almost for exponents as well.

NOTE. In retrospect all this also appears in Grant Malcolm's thesis, though in different words.

Tupling and Mutumorphisms

Maarten M. Fokkinga. The Squigollist, Vol 1, Nr 4, pages 81--82, 1990, 2 pages.

Abstract. We prove the following folklore theorem categorically. Consider a collection of functions that are mutually recursively defined by induction on the structure of an initial data type. Then the tupling of the collection into one function is a catamorphism on that initial data type. (The functions in the collection are called mutumorphisms.) Cata-, para- and Malcolm's zygomorphisms are immediately obtained from such tupled mutumorphisms, as are the important properties like the Unique Extension Property and Promotion.

Selector Guards

Maarten M. Fokkinga. The Squigollist, Vol 1, Nr 4, pages 68--73, 1990, 6 pages.

Abstract. The notion of selector guard is defined and some of its properties are inverstigated. A selector guard is a function that may be used as any other function; in the context of a selector it behaves as a "guard": it takes care that certain values will not be selected by the selector.

Selector guards are more flexible than constructions with a guard on a fixed position like guarded commands and McCarthy conditionals. Some filters may be replaced by mapped selector guards, and this has calculational advantages.

Tupling of Catamorphisms Yields a Catamorphism

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, May 1990, 4 pages.

Abstract. We prove categorically the folklore theorem that tupling of catamorphisms yields a catamorphism again. As an application we redo Bird's "Using Circular Programs to Eliminate Multiple Traversals of Data" in a very general setting.

Jan Kuper's solution to ``Shall we calculate - II?''

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, April 1990, download: 30 pages.

Abstract. We give Jan Kuper's solution to Richard Bird's challenge in the Squiggolist. Our formulation differs from Jan Kuper's mainly in the rather formal way in which we handle the introduction of bound variables in the course of a calculation. The "calculation" that establishes the equality, is a linearized natural deduction rather than a calculation with terms that denote programs (as we would like to do in the BM style of programming).

Bound Variables and Hypotheses in a Calculational Proof

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, April 1990, 5 pages.

Abstract. The proof format advocated by Dijkstra and his followers is extended with a facility to introduce bound variables and hypotheses in the course of a calculation, i.e., without interrupting the structure of the calculational proof.

A BM Style Derivation of The Lexico Least Upperbound of Pattern e in subs x

Maarten M.Fokkinga. Unregistered technical report, CWI, Amsterdam, March 1990, 25 pages.

Abstract. The BM style (after the originators Bird and Meertens) of programming advocates, amongst others, to derive a program from its specification in the way mathematicians derive solutions to equations in, say, arithmetic or other fields with an algebraic nature. That is, ideally, a derivation consists of a straightline chain of identities, all of which are instances of basic laws of the calculus or of higher level algorithmic theorems. We present a very detailed BM style derivation of a linear time program for the function that, given a sequence x, yileds the lexicographic least upperbound of a fixed pattern e amongst all possibly noncontiguous subsequences of x. By far the most steps in the calculation turn out to be simple distributivity properties of the operators involved. As a novelty, we introduce a kind of guards (to be used in the context of a selector) that have nicer calculational properties than constructs like filter and conditional, which have guards built in in a fixed way.

Using Underspecification in the Derivation of some Optimal Partition Algorithms

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, March 1990, 26 pages.

Abstract. Indeterminacy is inherent in the specification of optimal partition (and many more) algorithms, even though the algorithms themselves may be fully determinate. Indeterminacy is a notoriously hard phenomenon to deal with in a purely functional setting. In the paper "A Calculus Of Functions for Program Derivation'' R.S.Bird tries to handle it by using underspecified functions. (Other authors have proposed to use `indeterminate' functions, and to use relations instead of functions.) In this paper we redo Bird's derivation of the Leery and Greedy algorithm while being very precise about underspecification, and still staying in the functional framework. It turns out that Bird's theorems are not exactly what one would like to have, and what one might understand from his wording of the theorems. We also give a derivation in the Bird-Meertens style of a (linear time) optimal partition algorithm that was originally found by J.C.S.P. van der Woude.

Homo- and Catamorphisms, Reductions and Maps --- An Overview

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, February 1990, 20 pages.

Abstract. The classical notion of homomorphism, the Bird-Meertens notion of homomorphism —here called catamorphism— having reduction and map as a special case, are defined formally and investigated with respect to their calculational properties. All this is done both in terse category theoretic terminology, as well as spelled out in more conventional, less abstract, concepts. This note reflects my current understanding of other people’s work, in particular the ideas of Lambert Meertens.

Squiggolish Derivations for some Optimal Partition Algorithms --- Promotion as the Driving Force

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, December 1989, 25 pages.

Abstract. Consider the specification that, given a function f and a predicate p, asks for a minimally f-valued partition all of whose segments satisfy predicate p. We derive four algorithms in a systematic way; among others the so-called Leery and Greedy algorithm. Promotion (i.e., right shift in the algorithmic expression) turns out to be the driving force for the derivation. We adhere to the Squiggol style: we reason algebraically and avoid bound variables as much as possible. The framework we are working in is purely functional, and we are very careful about the indeterminacy that is given in the specification. Finally, we observe a correspondence between some fictitious values and exception handling.

For those who love calculating

Maarten M. Fokkinga. The Squigollist, Vol 1, Nr 2, pp. 17--18, 1989, 2 pages.

Abstract. The aim of Agoritnmics is to derive algorithms from a specification by algebraic transformations. It is well known that bound variables tend to stand in the way of decomposing an expression into its semantic constituents, and hence hinder the calculation. Thus there is an ever growing tendency to use combinators that allow to avoid variables. In this note we bring it to an extreme by providing a variable free expression for cross-with-plusle.

Operators as Higher Order Functions --- A Case Study

Maarten M. Fokkinga. Unregistered technical report, CWI, Amsterdam, May 1989, 11 pages.

Abstract. When a binary operation occurs as an argument of a function, or as an operand of an operator, one is faced with the problem of typing the operation. One solution is to extend the type formation rules with pairs and to introduce several functions and operators that work on pairs, like || defined by (f || g)(x,y) = (f x, g y). Another solution is to curry the operation into a (higher order) function that expects the arguments one after the other; in this case no extra type formations and operations are needed. We investigate the consequences of the latter choice with respect to the Algorithmics style of programming. It turns out that there are many steps needed that only shuffle the parameters to their place. Moreover, there appear a lot of explicit composition operators o with one operand, which itself may be an operator like map * , so that a lot of parentheses are needed to disambiguate the formulae or another notation has to be exploited.

Elimination of SIGMA-types by means of introspective types

Maarten M. Fokkinga. Handwritten note, February 1988, 16 pages.

Abstract. We extend the (term and) type formation rules of the (higher order) typed lambda-calculi with the rule: "(Rx:M. N) is a type, whenever x is a term variable and N, M are types". This type is called the introspective type, because x stands for the term to which this type is assigned. Consequently, one of the type inference rules reads: "from E has-type (Rx:N.M) conclude E has-type M[x:=M]".

We show that the strong Sigma-types (with its two projections) can be translated into Pi-types plus the introspective type; (in this translation there is no need for "Type has-type Type".

A correctness proof of sorting by means of formal procedures

Maarten M. Fokkinga. Science of Computer Programming, vol.9, pp.263-269, North-Holland, Amsterdam, ISSN 0167-6423, 1987, 6 pages.

Abstract. We consider a recursive sorting algorithm in which, in each invocation, a new variable and a new procedure (using the variable globally) are defined and the procedure is passed to recursive calls. This algorithm is proved correct with Hoare-style pre- and post- assertions. We also discuss the same algorithm expressed as a functional program.

Transformatie van Specificatie tot Implementatie

M.M. Fokkinga. In: J.A.A.M. Poirters, G.J. Schoenmaker / Colloquium Software Specificatie Technieken / Academic Service / Schoonhoven, Nederland / ISBN 90-6233-269-2, pp. 53-86, 1987, download: 52 pages.

Abstract. Constructies van correcte en efficiënte programma's zijn mogelijk door stapje-voor-stapje de specificatie (in wiskundige notatie) te transformeren onder behoud van betekenis. De tussenstadia zijn steeds beter executeerbare specificaties; het eindpunt is een wiskundige formule die tevens een legale expressie is in een Functionele Taal zoals SASL, Miranda, Hope of Twentel. Een volgende stap, de omzetting tot een Imperatief (Pascal) programma, is nu ook mogelijk.

Bij zo'n transformatieproces worden methoden en technieken toegepast die, veralgemeend en geschematiseerd, als afzonderlijke lemma's bewezen kunnen worden. Voor praktische uitvoerbaarheid van deze manier van programma-constructie is het nodig dat de specificatie- en programmanotatie zeer beknopt is en geschikt voor algebraïsche manipulatie,

Bovenstaande wordt aan de hand van "Backtracking" en nog een probleem toegelicht.

Backtracking and Branch-and-Bound Functionally Expressed

Maarten M. Fokkinga. In: Computing Science in the Netherlands / 1987 / CWI / Amsterdam, Netherlands / SION congres 1987, pp.207-224, Extended version: Memorandum INF-86-18, june 1986, University of Twente, download: 40 pages.

Abstract. We develop a program scheme in a functional language with lazy evaluation for the kind os algorithms which are usually called Backtracking algorithms and Branch-and-Bound algorithms. Several examples are given, amongst others the Eight Queens Problem and the Problem of the Optimal Selection.

An Elementary Semantics for Cardelli's System of Multiple Inheritance

H. Balsters, M.M. Fokkinga. Technical Report, no. Memorandum INF-87-33, University of Twente, Enschede, Netherlands, 1987, 15 pages.

Abstract. In 1984 Luca Cardelli gave a formal definition of a typed object-oriented language incorporating a sub-type relation used to describe multiple inheritance. Cardelli's fundamental result was a semantics for his system that enabled sub-typing to be modelled as straightforward set-inclusion. In this paper an alternative semantics for Cardelli's system is offered in which this result is proved in a more elementary framework.

Keywords: object-oriented programming, inheritance, lambda-calculus, types, set-theory.

Inleiding Logika voor Informatici

H. Brinksma, L. Fleischhacker, M.M. Fokkinga, L.A.M. Verbeek. Technical Report, Universiteit Twente, Enschede, Nederland, (Lecture notes, in Dutch), 1987, 106 pages.

Abstract. De vakgebieden Informatika en Mathematische logika hebben zich in onze eeuw ontwikkeld tot gebieden die op vele punten nauwe verwantschap vertonen. De mathematische logika geeft een theoretische rekonstruktie van de strukturele eigenschappen van het wiskundig redeneren. In de informatika wordt op grond van de kennis van deze strukturele eigenschappen het resultaat van dit wiskundig redeneren door middel van informatieverwerkende systemen nagebootst. Geen wonder dat de informatika vele fundamentele methoden en begrippen met de mathematische logika gemeen heeft. In de mathematische logika worden deze methoden en begrippen in hun theoretische samenhang ontwikkeld, terwijl ze in de informatika in dienst staan van het ontwikkelen en beschrijven van de methoden van dit vakgebied. De mathematische logika is dan ook bij uitstek geschikt om de grondbeginselen van de informatika in hun exakte verband te leren begrijpen. Het hier behandelde gedeelte van de mathematische logika maakt de "kern" van dit vakgebied uit. De behandeling is beperkt tot het wiskundige ’geraamte’ en de meest fundamentele begrippen en methoden. In de hoofdstukken 10, 11 en 12 worden enige verbanden met onderwerpen uit de informatika gegeven. De konceptueel-wijsgerige achtergronden komen in de W&M vakken 'Inleiding logika’ en ’Mathematische logika’ aan de orde.

Modellering van lijsten in 2de orde getypte lambda-calculi

Maarten M. Fokkinga. Handgeschreven notitie, december 1987, 20 blz.

Abstract. In "Programming Language Concepts --- The Lambda Calculus Approach" wordt getoond hoe lijsten in de 2de orde (= Reynolds-Girard) getypte lambda-calculus gemodelleerd kunnen worden, door een specifiek programmaschema te geven. Henk Barendregt was geïnteresseerd in de formulering van een stelling waarvan dat programmaschema (een deel van) het bewijs vormt. Dit verhaal is een eerste poging daartoe: we geven een heel algemene definitie van het begrip (1ste en 2de orde) getypte lambda-calculus, en presenteren (de essentie van) de constructie als een transformatie tussen lambda-calculi die -in zekere zin- convertibiliteit exact behoudt.

Bird's aanpak van nonterminatie

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 8 blz.

Abstract. Het gebruik van "undef" in Bird's boek kan tot misverstanden leiden, omdat Bird niet erg precies is in de rol die "undef" speelt. Ik geef aan wat die rol is, en wat alternatieven voor de behandeling van nonterminatie zijn.

De convexe omhullende geprogrammeerd in Bird's stijl

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 8 blz.

Abstract. Ter illustratie van de beoogde moeilijkheidsgraad van de programmeerproblemen aan het einde van het college "Programmeren I nieuwe stijl" stelt Duijvestijn voor: het bepalen van de convexe omhullende. Ik geef in dit verhaal de manier waarop ik dat geprogrammeerd heb, en waarbij ik de stijl van Bird's boek heb proberen te volgen.

Duijvestijn's geometrie in Bird's stijl uitgedrukt

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 11 blz.

Abstract. Voor de commissie HOP (Herstucturering Onderwijs in hetProgrammeren) van de INF-werrkgroep WIP (Werkgroep Inleidend Programmeeronderwijs) heeft Duijvestijn een aantal teksten voorbereid met voorbeeldprogramma's en voorbeeld programmaontwikkelingen in een functionele taal (Twentel). Ik geef in essentie exact dezelfde algoritmen, maar probeer dat te doen in de stijl van Bird's boek. Het resultaat vind ik verbluffend en onverwacht! Recursie blijkt niet meer expliciet nodig en ik kan volstaan met de notatie van Chapter 1-3. Het grote verschil in stijl tussen Bird's boek en Cuijvestijn's programma's zit hem, mijns inziens, in het verschil tussen programmeren op functie-nivo (Bird) versus object-nivo (Dvst).

Een verklaring voor de eenvoud en het gemak van Bird's stijl

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 6 blz.

Abstract. In vorige verhaaltjes heb ik laten zien hoe ogenschijnlijk ingewikkelde algoritmen heel eenvoudig, duidelijk en begrijpelijk in de stijl van Bird kunnen worden uitgedrukt. Steeds heb ik gezegd dat het programmeren op functie-nivo (d.w.z., abstract, in de stijl van Bird) misschien wel meer denkwerk vereis dan het programmeren op object-nivo (d.w.z., direkt in termen van individuele data-elementen met expliciete recursie). maar dat het denkwerk alleszins de moeite waard is gezien de elegantie (kwaliteit, begrijpelijkheid, etc) van de reslterende programma's. Ik krijg nu zo langzamerhand de overtuiging dat het programmeren in de stijl van Bird niet méér denkwerk vereist, maar integendeel juist minder. In dit verhaal zal ik d redenen daarvoor proberen te expliciteren.

Enige algemene attitude doelstellingen voor 1ste jaars programmeren

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 5 blz.

Abstract. Ik geef enige doelstellingen die we mijns inziens moeten nastreven met het eerstejaars programmeeronderwijs. Ik heb niet de pretentie volledig te zijn; bovendien beperk ik me tot de "algemene attitude".

Optellen en vermenigvuldigen in Bird's notatie

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 16 blz.

Abstract. We beschouwen de lagere school algoritmen voor het optellen en vermenigvuldigen, en drukken die uit in Bird's notatie. Dit doen we enerzijds zónder en anderzijds mét explicite recursie. De formulering met expliciet recursie dwingt af dat we in de decimale representatie van getallen de eenheden "op kop" kiezen; dis is bij de "recursie-loze" formulering niet nodig.

Van FP naar IP --- een case study

Maarten M. Fokkinga. Handgeschreven notitie, april 1987, 11 blz.

Abstract. We beschouwen Bird's priemgetallen programma en proberen dat op gedisciplineerde manier in een imperatief programma om te zetten. Het blijkt dat in dit geval dat kennis van het functionele programma de constructie van het Pascal programma nauwelijks vergemakkelijkt.

Bird's boek gezien vanuit de HOP-activiteiten

Maarten M. Fokkinga. Handgeschreven notitie, maart 1987, 6 blz.

Abstract. Evaluatie van Bird's boek gezien vanuit de activiteiten van de commissie Herstructurering Onderwijs in het Programmeren.

Het Acht Koninginnen Probleem

Maarten M. Fokkinga. Handgeschreven notitie, februari 1987, 5 blz.

Abstract. In een uiteenzetting voor docenten, niet studenten, worden verschillende imperatieve programma's voor het Acht Koninginnen Probleem afgeleid uit een formele specificatie. Diverse aspecten worden expliciet onderscheiden.

Hilbertkrommen tekenen

Maarten M. Fokkinga. Handgeschreven notitie, februari 1987, 6 blz.

Abstract. We construeren een functioneel programma dat Hilbert krommen tekent en belichten verschillende aspecten van de werkwijze.

Another variant of the Schorr-Waite algorithm and its correctness proof --- an exercise in formulation

M.M. Fokkinga, P.G. Jansen. In: NGI-SION 1986 Symposium Stimulerende Informatica / Stichting Informatica Congressen / ISBN 90-5005-007-7, pp.445-455, 1986, 12 pages.

Abstract. The Schorr-Waite algorithm is of interest for garbage collection; it marks all cells of the store reachable from a given pointer, using only a few simple global variables and two bits in each cell. We present another variant of this well-known algorithm and prove its correctness in an intuitively appealing way.

De rij van unieke bladwaarden van een boom

Maarten M. Fokkinga. Handgeschreven notitie, mei 1986, 3 blz.

Abstract. We behandelen het probleem om bij gegeven willekeurige boom de rij van die bladwaarden op te leveren die precies éénmaal in de boom (als bladwaarden) voorkomen.

Van Recursie naar Iteratie

Maarten M. Fokkinga. Handgeschreven notitie, mei 1986, 5 blz.

Abstract. We geven verscheidene manieren om enkelvoudig recursieve functie-definities naar iterartieve om te zetten. Hieruit resulteer een "stabndaard techniek" voor programmeren. Dit verhaal is geinspireerd --en een uitbreiding van-- de hand-outs bij het college Functionele talen van Gerrit van de Hoeven.

Een omzetting van L-REC naar L-ITER definities

Maarten M. Fokkinga. Handgeschreven notitie, mei 1986, 3 blz.

Abstract. LREC en L-ITER zijn recursie-schema's voor functies op lijsten; L-ITER is de iteratieve ofwel tail-recursieve vorm. LREC is de niet-ieteratieve lineaire recursieve vorm en beide plegen recursie op de staart van de argumentlijst. Wij geven een omzetting van LREC-definities naar L-ITER definities, die gelijkwaardige functies oplevert wanneer hun domein tot eindige totale lijsten beperkt wordt.

Elimination of left-nesting

Maarten M. Fokkinga. Unregistered Technical Note, Twente University of Technology, Enschede, Netherlands, May 1986, 7 pages.

Abstract. Let c be an operation so that (c x (c y z)) = (c (c x y ) z) whereas the costs of evaluating (c x (c y z)) are smaller than the costs of evaluating (c ((c x y) z). Then it is an efficiency improvement to eliminate, or rather prevent, calls of c that are nested in the left argument in exchange for nested calls in the right argument. We shall treat this elimination of left nesting in a general setting. We shall reason in a mathematically rigorous way. Actually, by choosing a functional (rather than imperative) language to specify computations, the programming process becomes a fully mathematical activity.

1982 CR categories: D1.1, F3.1

Key words & phrases: functional programming, reasoning about programs, correctness preserving program transformation.

Some Thoughts on Nondeterminism

Maarten M. Fokkinga. Handwritten note, April 1986, 14 pages.

Abstract. A collection of private opinions and thoughts on the desirability, necessity and manageability of nondeterminism is presented. Together they constitute the slightly adapted and extended contents of two previous notes of mine (in Dutch). I am fully aware of the fact that all topics treated here are presumably treated much better in the literature; I welcome any specific of general references to the literature and any comments or criticism the reader may have. These notes haven been written hastily on special request.

Functioneel programmeren in een vogelvlucht

Maarten M. Fokkinga. INFORMATIE, vol.27, no.10, pp.862-873, Kluwer b.v., Deventer, Netherlands, 1985, 12 blz.

Abstract. Functionele programmeertalen onderscheiden zich van conventionele (imperatieve, procedurele) programmeertalen in wezen doordat ze geen assignment en assigneerbare variabelen hebben. Ze zijn in snelle opmars omdat ze (naast nadelen ook) een aantal onmiskenbare voordelen hebben boven imperatieve talen. We willen hier geen vergelijking maken tussen beide klassen van talen n evenmin de voordelen van functionele talen op- sommen en toelichten. Integendeel onze bedoeling is het karakter en de stijl van functioneel programmeren duidelijk te maken aan de hand van voorbeelden; de lezer oordele dan zelf maar. We richten ons daarbij tot een oningewijde die nog nooit iets van functionele programmeertalen gezien hoeft te hebben maar wel enigszins bedreven is in een of andere conventionele programmeertaal.

Exception Handling Constructs Considered Unnecessary

Maarten M. Fokkinga. In: Uitdaging van de Informatica / Nederlands Genootschap voor Informatica (NGI) / Amsterdam / ISBN90-70621-17-7 / Proceedings NGI-SION 1985 Symposium, pp.406-416, 1985, 12 pages.

Abstract. In his thesis "Exception handling: the case against’ (Univ. of Oxford, January 1982) Andrew P. Black shows convincingly that normal control structures, together with the data type discriminated union, suffice to replace exception handling facilities in a satisfactory way. We want to propagate his ideas with an example. Moreover we show that (i) even with the discriminated union approach incremental program construction is still possible, and that (ii) the programs using discriminated unions resemble the programs using exception handling facilities more than Black suggests.

Fair nondeterministic merge considered necessary

Maarten M. Fokkinga. Handgeschreven notitie, november 1985, 10 blz.

Abstract. Een verzameling kan in een functionele programmeertaal gerepresenteerd worden als een opsomming (lijst) van zijn elementen. We laten zien dat het werken met deze representaties veel prettiger gaat als de "eerlijke nondeterministische meng"-operator in de taal aanwezig is. De gevolgen, die de aanwezigheid van die operator heeft op het redeneren over de korrektheid van programma's, worden kort beschouwd.

Een recursie-schema voor totale in plaats van partiële lijsten

Maarten M. Fokkinga. Handgeschreven notitie, november 1985, 3 blz.

Abstract. We presenteren een recursie-schema voor totale in plaats van partiële lijsten, bedacht door Gerrit van der Hoeven.

Een les in functioneel programmeren

Maarten M. Fokkinga. Handgeschreven notitie, oktober 1985, 6 blz.

Abstract. We vertellen het een en ander over de methode van functioneel programmeren, aan de hand van het probleem om bij gegeven tekst een index te vormen.

Hiding of auxiliary functions in Miranda abstract types

Maarten M. Fokkinga. Handwritten note, October 1985, 3 pages.

Abstract. The abstract type facility of Miranda is based on transparency rather than hiding, that is: all te identifiers in the "definition" of the abstract type are visible throughout the script. However, sometimes one needs (for efficiency and/or comprehensibility, indeed even for theoretical necessity) auxiliary functions in the definition; and of course these should be hidden for the user of the type. We show that it is easy to achieve this in Miranda.

Bereikbaarheidstest voor grafen

Maarten M. Fokkinga. Handgeschreven notitie, september 1985, 3 blz.

Abstract. We geven een functioneel programma dat louter een "uitgeklede" versie is (zowel t.a.v. programmatekst als ook t.a.v. ontstaansgeschiedenis) van een programma uit een (lezenswaardig) verhaal van Gerrit van der Hoeven.

SVP-Typering van eindige automaten

Maarten M. Fokkinga. Handgeschreven notitie, september 1985, 7 blz.

Abstract. We beschouwen deterministische eindige acceptoren (automaten) en laten zien hoe de informele wiskundige typering van dergelijke dingen heel precies met de SVP-typering geformuleerd kan worden. Dit verhaal dienst als voorbeeld van de SVP-typering; niet als uitleg of definitie van die typering. Kennis van de SVP-typering is overigens niet nodig om dit verhaal te kunnen lezen of begrijpen.

Korrektheidsbewijs van een priemgetallen-programma

Maarten M. Fokkinga. Handgeschreven notitie, augustus 1985, 3 blz.

Abstract. We bewijzen de korrektheid van een slim programma dat de lijst van alle priemgetallen voortbrengt. Daarbij ontkomen we er niet aan om het volgende, niet bewezen, beginsel te gebruiken: "Als twee lijsten voor willekeurige k (k eindig) gelijk zijn aan elkaar op de eerste k elementen, dan zijn de lijsten zelf gelijk aan elkaar".

Lazy evaluation op expressie-nivo uitgelegd

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, augustus 1985, 7 pages.

Abstract. Lazy evaluation is een evaluatie-methode voor functionele programma's waarmee duplicaties van evaluatiestappen voorkomen worden. Wij geven hier een uiteenzetting van lazy evaluation geheel in termen die de praktiserend programmeur (in tegenstelling tot implementeur) gebruikt.

Hoe moet semantische equivalentie gedefinieerd worden?

Maarten M. Fokkinga. Handgeschreven notitie, augustus 1985, 20 blz.

Abstract. We stellen ons ten doel om uitgaande van een gegeven taal en een gegeven operationele semantiek een begrip "semantische (of: abstracte) equivalentie" te definiëren. Al onze pogingen falen en we dagen de lezer uit een bevredigende definitie te geven of de onvervulbaarheid (onzinnigheid) van onze wensen aan te tonen.

Gesynchroniseerde interactie onder lazy evaluation

Maarten M. Fokkinga. Handgeschreven notitie, juli 1985, 5 blz.

Abstract. Bij een dialoog tussen computer en gebruiker, die in een lazy-geëvalueerde taal geprogrammeerd is, doet zich het verschijnsel voor dat soms al delen van een antwoord op het beeldscherm verschijnen voordat de gegevens door de gebruiker zijn ingetikt. Wij geven aan hoe zulks vermeden kan worden.

Functionele programmering van een beeldscherm-schildpad

Maarten M. Fokkinga. Handgeschreven notitie, mei 1985, 4 blz.

Abstract. We geven een SASL' programma zó dat een gebruiker vanachter de terminal de cursor op het beeldscherm kan besturen middels het intikken van commands's zoals V (doe een stap voorwaarts), R (Draai naar rechts), L (draai naar links), enzovoorts. Ook eenvoudige iteraties en "onthoud"-commando's komen aan bod.

A functional program that replaces variables by their lexical address

Maarten M. Fokkinga. Handwritten note, mei 1985, 5 blz.

Abstract. We present a functional program for an abstraction of the problem to replace in a program text each applied occurrence of a variable by its lexical address, that is, a two-tuple [n,p] where n is the lexical level of its declaration and p is the position of that declaration within that level. The fact that variables may precede their definition makes the problem interesting. The program is strongly related to an attribute grammar for the problem.

Nederlandse telwoorden voor getallen

Maarten M. Fokkinga. Handgeschreven notitie, april 1985, 5 blz.

Abstract. We geven een SAL-achtige funktie die willekeurig natuurlijk getal in het Nederlands omzet; bijvoorbeeld 123.456.789 = "honderdrieentwintig miljoen vierhonderdzesenvijftig duizend zevenhondernegenentachtig".

Over intermittent en inductive assertions

Maarten M. Fokkinga. Handgeschreven notitie, maart 1985, 5 blz.

Abstract. Intermittent assertions en inductive assertions zijn termen die in de literatuur gebruikt worden om twee verschillende methoden aan te duiden voor het bewijzen van de korrektheid van een programma. Wellicht dat een betere terminologie luidt "data gerichte" en "syntaxis gerichte" methoden. (De laatste methode is de bekende methode met invarianten à la Hoare.) Ik zet beide methoden uiteen.

A notation for the most general form of repetition

Maarten M. Fokkinga. Technical report, no. Memorandum INF-84-3, Twente University of Technology, Enschede, Netherlands, 1984, 12 pages.

Abstract. We present a notation with which all forms of repetition (like the well known while, repeat, Dijkstra's do od, Parnas' it ti, Zahn's events, multi-level exits, and so on) can be written in a very simple and uniform way.

References versus Pointers

Maarten M. Fokkinga. Handgeschreven notitie, 1984, 7 blz.

Abstract. "Mijn Algol68 opvatting" en "de Pascal opvatting" van het begrip assigneerbare variable worden beschreven en met voorbeelden toegelicht. het komt erop neer dat in mijn Algol68 opvatting cellen van de opslagruimte met hun adressen worden geïdentificeerd, terwijl ze in Pascal worden onderscheiden als verschillende datatypen.

Assignments in asserties - toegelicht met het Schorr-Waite algoritme

Maarten M. Fokkinga. Handgeschreven notitie, oktober 1984, 7 blz.

Abstract. Asserties zijn beweringen over de toestand (op één tijdstip) gedurende de berekening, en worden gebruikt om de korrektheid van algoritmen aan te tonen. Gewoonlijk worden asserties geformuleerd in een wiskundig-achtige taal of een zeer informele versie daarvan; het gebruik van "neveneffecten" binnen asserties is hoogst zeldzaam, maar allerminst onmogelijk of inconsistent. We zullen het Schorr-Waite algoritme korrekt bewijzen door in de asserties assignments, en programmafragmenten, op te nemen.

Een funktioneel programma

Maarten M. Fokkinga. Handgeschreven notitie, juni 1984, 2 blz.

Abstract. Uitgedaagd door een artikel van Berztiss en Thatte in 1983, construeren we een funktioneel programma dat een binaire boom transformeert door in de "n-de" knoop (in de volgorde van de in-order traversal) de waarde met n te verminderen.

Tekenen in SASL

Maarten M. Fokkinga. Handgeschreven notitie, januari 1984, 2 blz.

Abstract. Een SASL representatie voor tekeningen en bewerkingen daarmee wordt gegeven. Als voorbeeld wordt een kort en bondig programma gepresenteerd voor de zogenaamde Hilbertkrommen (ook wel Peanokrommen genoemd).

Structuur Van Programmeertalen

M.M. Fokkinga. Technical report, University of Twente, Enschede, Netherlands, (Lecture Notes in Dutch, Structure of Programming Languages), 1983, 250 pages.

Abstract. In deze syllabus zullen wij allereerst de struktuur van beschrijvende talen uiteenzetten en twee implementatiemodellen schetsen, en vervolgens steeds meer gebiedende aspekten toevoegen. Het onderwerp typering wordt elders uitvoerig behandeld en komt hier in het geheel niet aan bod.

Deze verhandeling onderscheidt zich van de meeste literatuur in de volgende twee aspecten. (1) We besteden veel aandacht aan beschrijvende (=funktionele, applikatieve) programmeertalen. Het valt te verwachten dat in de toekomst beschrijvende programmeertalen een hoge vlucht nemen. Daarenboven kunnen ze een geweldige steun bieden tijdens het ontwerpproces van gebiedende (=imperatieve, konventionele) programma's. Enig inzicht in de struktuur van dergelijke talen (of subtalen) is dus gewenst. (2) Wij gaan uit van een ideale notatie [niet qua syntactische vormgeving, wel qua semantische inhoud] en presenteren zo nodig beperktere versies daarvan; die beperkingen zijn soms nodig voor een doelmatige verwerking van de programma's op de hedendaagse machines.

Over het nut en de mogelijkheden van typering

M.M. Fokkinga. Technical report, no. Memorandum INF-83-5, Twente University of Technology, Enschede, Netherlands, (Lecture Notes, in Dutch, "On the use and the possibilities of typing''). Also issued as Lecture Notes, 1983, 54 blz.

Abstract. In dit verhaal proberen we enig inzicht te verschaffen in het begrip "typering" zoals dat bij programmeertalen voorkomt. Het nut dat typering moet hebben staat daarbij voorop. Aan de hand van een minitaal en voorbeelden wordt de conventionele, zogenaamde eerste orde, typering beschreven; deze wordt gebruikt in talen zoals Pascal en Algol. Ook minder conventionele, en wel: hogere orde, typeringen en de zogenaamde type-polymorfie worden uitgelegd.

On the notion of strong typing

M.M. Fokkinga. In: J.W. de Bakker, J.C. van Vliet / Algorithmic Languages / 1981 / Mathematical Centre Amsterdam, IFIP TC2 / North-Holland / Amsterdam, The Netherlands / ISBN 0-444-86285-4 / International Symposium, Amsterdam, pp. 305-320, October 1981, 16 pages.

Abstract. The usefulness of strong typing is formalized in the following way. Strong typing is a syntactic means to restrict the class of programs so that a pleasant semantic property holds. More precisely, a semantic equivalence of strongly typed programs is proved independent of the representation used to implement abstract entities like numbers, truth values and predefined ones. Thus a formal content is given to phrases like ‘‘typing prevents to employ unintended properties of representations’" and ‘‘semantically types are redundant".

On the correctness proof of the SASL Lambo program

Maarten M. Fokkinga. Handwritten note, July 1981, 14 pages.

Abstract. We show that the proof given by Dijkstra for the imperative Lambo program is incomplete with regard to the correctness. Any completion of that proof. however, can be translated to a correctness proof for the corresponding SASL program. The techniques employed are quite generally applicable.

Specifying precedence relations using two level grammars

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, February 1980, 4 pages.

Abstract. Usually the priority or precedence of operators, and of arbitrary composition schemes for expressions, is modeled within the context free grammar of a language by choosing distinct nonterminals for each priority class. This however gives rise to derivations (parse trees, productions trees) in which semantically redundant steps occur. We show, by means of an example, how the priority relations can be modeled in a simple two level (2VW) grammar such that the derivations do not contain semantically redundant steps.

Some self-reproducing Algol-like programs and Kleene's recursion theorem formulated in concrete programming languages

Maarten M. Fokkinga. Technical report, no. TW-memo 281, Twente University of Technology, Enschede, Netherlands, September 1979, 22 pages.

Abstract. We give some self-reproducing Algol 60 and Algol-like programs. We show that one of them can be derived quite formally from Kleene's Recursion Theorem. To this end we reformulate the theorem and its proof in terms of manipulations on program texts, wherever possible, rather than on indices of functions. As further applications the theorem is formulated in terms of the language HET, the pure lambda calculus and LISP. We consider our understanding of the decades old proof as the main achievement of the work done.

Evaluation of numbers written in the Fibonacci system

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, July 1979, 6 pages.

Abstract. We consider a ver simple algorithm which evaluates a number in de Fibonacci system from left to right according to Horner's scheme. Both an a priori mathematical problem analysis and a direct algorithmic construction are given. Finally, we investigate the generalization for arbitrary recurrence relations.

A Simpler correctness proof of an in-place permutation algorithm

Maarten M. Fokkinga. Technical report, no. TW-Memo 249, Twente University of Technology, Enschede, Netherlands, March 1979, 8 pages.

Abstract. In 1972 Duijvestijn gave a correctness proof of a particular permutation algorithm using an invariant relation. We present another proof based on this relation. It uses ghost variables and consequently can be split up into easily comprehensible parts. This might be of interest to the reader. The verification itself is hardly of interest: the application of the predicate transformation rules is straightforward and involves nearly no mathematics.

Axiomatization of Declarations and the formal treatment of an Escape Construct

Maarten M. Fokkinga. In: E.J. Neuhold / Formal Descriptions of Programming Language Concepts / 1978 / IFIP TC-2 / North-Holland / Amsterdam, The Netherlands / pp. 221-236, / ISBN 0-444-85107-0 / IFIP TC-2 Working Conference, St. Andrews, Canada, August 1-5, 1977, 16 pages.

Abstract. We give Hoare-like axiomatizations for variables, procedure and a new escape construct. The proof rules treat scope rules properly; simplifications are shown for a restricted use of global variables and for a disallowance of innerblocks. It is shown that the axiomatization of the escape construct has influenced its design.

A note on Rem's algorithm

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, 1978, 3 pages.

Abstract. It is assumed that the reader is familiar with chapter 23 of A Discipline of Programming (Dijkstra 1976). We give a different motivation for the property Ax. x >= f(x) , and obtain Rem's algorithm quite naturally, meanwhile lifting out its “compelling beauty".

Another difference between Recursive Refinement and Repetition

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, 1978, 6 pages.

Abstract. It is shown that - when derived with the same reasoning - Hehner's recursively refined iterations deliver more acceptable results than Dijkstra's repetitive constructs.

A note on the pragmatics of the repetitive construct

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, 1978, 8 pages.

Abstract. We formulate and discuss three pragmatics, i.e., thumb rules for the use, of the repetition construct, and illustrate them by means of examples taken from Dijkstra's "A Discipline of programming".

Comments on `Merging Problems Revisited'

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, 1978, 7 pages.

Abstract. It is shown that the invariant relation in the chapter "Merging Problems Revisited" of "A Discipline of Programming" by E.W. Dijkstra (Prentice Hall, 1976) is unnecessarily strong and complicated, and that a suitable, weaker and simpler invariant relation may be obtained more easily. This holds independently of the knowledge of the final representation of the sets.

Keywords and phrases. Invariant relation, variant function, guarded commands, programming methodology.

Disciplined Constructions of `Partition'

Maarten M. Fokkinga. Unregistered Technical Report, Twente University of Technology, Enschede, Netherlands, 1978, 17 pages.

Abstract. various formal developments, fully in the spirit of Dijkstra's "A discipline of programming", and subsequent optimizing program transformations for the algorithm PARTITION (Hoare 1961) ate described and analyzed.

Keywords and phrases. Programming methodology, guarded commands,invariant relation, variant function, repetitive construct, nondeterminacy, program transformation.

Repairing the Process semantics of Milner

Maarten M. Fokkinga. Handwritten note, Technische Hogeschool Twente, Enschede, Netherlands, 1977, 12 pages.

Abstract. A reparation of the defect in the semantics of the illustrative programming language, proposed by Milner in 1973, is proposed. The semantic equations have (almost) not been changed; it is the concept of process which has been slightly altered.

Exchanging Robustness of a Program for a Relaxation of its Specification

C. Bron and M.M. Fokkinga. Technical report, no. TW-Memorandum 178, Technische Hogeschool Twente, Enschede, Netherlands, September 1977, 26 pages.

Abstract. This paper motivates a programming concept which realizes the exchange of some robustness of a correct program part for a relaxation of its specification. The technical tool proposed restricts program abortions to a specified part of the program only, so that the execution of that part can - from the outside - not be distinguished from normal termination. The abstract (= axiomatic) semantics closely reflect the intuitive appeal of the construct. The tool is powerful in the sense that it provides a means to restrict abortions to program parts which may be unknown at the site where the abortion has been “programmed".

On the use of continuations in Mathematical Semantics

Maarten M. Fokkinga. Technical report, no. TW-Memorandum 159, Technische Hogeschool Twente, Enschede, Netherlands, January 1977, 19 pages.

Abstract. With respect to jumps it is shown how to structure the definition of the mathematical semantics of a programming language with the following two related objectives. First, the definition should not be easily adapted such that it describes less restrictive jumps. Second, from the definitional text itself the possible flows of control should be fully determined. These objectives are in the spirit of structured programming (now applied to semantics description) in that as much as possible should be clear by local inspection of the text.

A proposal for dealing with abnormal termination of programs

C. Bron and M.M. Fokkinga. Technical report, no. TW-memo 150, Technische Hogeschool Twente, Enschede, Netherlands, November 1976, 17 pages.

Abstract. A proposal is made for a mechanism to control abnormal termination of the execution of programs or parts of programs. The notational conventions introduced are such that programs in which the possibility of abnormal termination is taken into account, can be derived from the original programs without disrupting the original program's structure. The mechanism is powerful in the sense that it allows the termination of blocks which are unknown te the blocks from within which this termination is caused. The formal semantics closely reflect the intuitive appeal of the construct and are similar in nature to the semantics of procedure call.

Berekenbare Functies

M.M. Fokkinga en L.A.M. Verbeek. Technical report, Technische Hogeschool Twente, Enschede, Netherlands, Lecture Notes, juli 1976, 89 blz.

Abstract. Dit dictaat Berekenbare Funkties geeft de inhoud van het gelijknamige college. De bedoeling van het college is de fundamentele begrippen berekenbare funktie en beslisbaarheid en opsombaarheid duidelijk uiteen te zetten en de betekenis van deze begrippen voor de wiskunde en vooral voor de informatica aan te geven. Zodoende wordt enige theoretische ondergrond voor het verwerken van gegevens in de informatica gegeven. Daarnaast wordt hierdoor het lezen mogelijk gemaakt van theoretisch georiënteerde literatuur in de informatica waarin vaak begrippen voorkomen die samenhangen met berekenbaarheid.

Keywords and phrases. Berekenbare funktie, Turingmachine, beslisbaarheid, (recursieve) opsombaarheid, (on)oplosbaarheid, primitieve recursie, partiële funktie, Markovalgoritme.

Recursieve procedures en eenvoudige inductie asserties

Maarten M. Fokkinga. In: J.W. de Bakker / Colloquium Programmacorrectheid / vol.21 / Mathematical Centre Syllabus / Mathematical Centre / Amsterdam, The Netherlands / ISBN 90-6196-103-3, chapter X, pp.151-165, 1975, 16 pages.

Abstract. We geven inzicht in de kracht en werking van "eenvoudige" assertiemethode, met name voor recursieve procedures: in de premisse van de regel voor procedures laten we alléén maar correctheisbeweringen toe voor elementaire opdrachten. We laten zien dat er voor iedere recursieve procedure een regel te formuleren is die volledig is maar waarvan het aantal beweringen in de premisse dan en slechts dan eindig is als de recursieve procedure "regulier" is.

Comments on a paper by Milner concerning the semantics of parallelism

Maarten M. Fokkinga. Technical report, no. TW-Memo 71, Technische Hogeschool Twente, Enschede, Netherlands, 1975, 20 pages.

Abstract. In part 1 we present a representation of processes in the form of drawings. The representation is less precise as the lambda-notation of Milner, but may sometimes provide better insight. In part 2 we indicate a serious design mistake for the programming language proposed by Milner. We propose another semantics for the same syntax, but we are not satisfied with it. Throughout this paper, the paper referred to is R Milners “an approach to the semantics of parallel programs". We assume the reader to be familiar with it.

Inductive assertions patterns for recursive procedures

Maarten M. Fokkinga. In: B. Robinet / Programming Symposium / vol.19 / Lecture Notes in Computer Science / Springer-Verlag / ISBN 3-540-06859-7, pp.221-233, 1974, 13 pages.

Abstract. Hoare has given the proof rule "from (a): p and B{S}p, conclude (b): p{while B do S} p and not B", according to which we may infer the validity of the "correctness assertion" (b) from the "inductive assertion" (a). We investigate the possibility of setting up such rules for recursive procedures, in which we only admit inductive assertions about elementary statements, and which will characterize the recursive procedures in a precise sense. It will appear that the premiss of such a characterizing rule in general consists of an infinite set of inductive as statements (about elementary statements) and that a finite characterizing set exists if and only if the procedure is "regular".

Motivatie en Scott's Tralietheoretische benadering voor een Wiskundige Semantiek van Programmeertalen

M.M. Fokkinga. Handgeschreven rapport, Technische Hogeschool Delft, Delft, Netherlands, 1974, 29 pages.

Abstract.We geven redenen aan waarom een semantiek van programmeertalen nodig is en waarom die "wiskundig" (in plaats van "operationeel") moet zijn. We Beschrijven wat een wiskundig model is en hoe een wiskundige semantiek er uit ziet. We werken dit uit in een voorbeeld. We laten zien waarom we terecht komen bij complete continue tralies met berekenbare bases. Dit alles resulteerde uit een literatuurstudie en is voorgedragen op het 10de Nederlandse Mathematisch Congres (Twente, april 1974) in het kader van een overzicht over Semantiek van Programmeertalen.

Notities n.a.v. ``Notities over de behandeling van het parametermechanisme in de syllabus Agol 60 (CB68)''

M. Fokkinga. Handgeschreven notitie, Technische Hogeschool Twente, Enschede, Netherlands, november 1974, 6 blz.

Abstract. Enkele opmerkingen, bezwaren en ideeën over Coen Bron's notitie (CB68). Zij betreffen doelstellingen, kritiek van algemene aard en kritische opmerkingen van technische aard.

Schets van een hoofdstuk over: Het Ontwerpen Van Algoritmen

M.M. Fokkinga. Handgeschreven rapport, Technische Hogeschool Twente, Enschede, Netherlands, september 1974, 38 blz.

Abstract. We geven een methodiek voor het ontwerpen van (voor computerverwerking bedoelde) algoritmen, bedoeld voor een eerste kennismaking met programmeren.

On the interpretation of program schemes --- an algebraic approach

M.M. Fokkinga. Handwritten report, Technische Hogeschool Delft, Delft, Netherlands, March 1974, 36 blz.

Abstract. This manuscript is an elaboration of the notes made during the lecture of M. Nivat at the "Advanced Course on Semantics of Programming Languages" (Saarbrücken, Germany, Febr 1974).

A self-reproducing Algol 60 program

M.M. Fokkinga. Algol Bulletin, vol.35, pp.24-26, IFIP Working Group 2.1 on Algol, 1973, 4 pages.

Abstract. An Algol 60 program is presented which prints literally itself, by means of a procedure OUTS(<string>) only.

Inductive assertions patterns for recursive procedures

M.M. Fokkinga. Technical report, Technische Hogeschool Delft, Delft, Netherlands, 1973, 26 pages.

Abstract. Hoare has given the proof rule "from (a): p and B{S}p, conclude (b): p{while B do S} p and not B", according to which we may infer the validity of the "correctness assertion" (b) from the "inductive assertion" (a). We investigate the possibility of setting up such rules for recursive procedures, in which we only admit inductive assertions about elementary statements, and which will characterize the recursive procedures in a precise sense. It will appear that the premiss of such a characterizing rule in general consists of an infinite set of inductive as statements (about elementary statements) and that a finite characterizing set exists if and only if the procedure is "regular".

An abbreviated version has been published in 1974.