Institute of Information Science, Academia Sinica

Library

Print

2019 Technical Report

Code
Subject / Author / Abstract
View

Code

TR-IIS-19-001

Subject / Author / Abstract

A Prehistoric Calculator
Kelly McKennon

It is shown how a certain prehistoric symbol can be used as a calculator to compute sums, differences, products, quotients and square roots. As an example, this symbol is used to compute the dimensions of a typical building block of the great pyramid of Giza.

View

Fulltext

Code

TR-IIS-19-002

Subject / Author / Abstract

Equational reasoning for non-determinism monad: the case of Spark aggregation
Shin-Cheng Mu

As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad. We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author's previous work on proving properties of Spark aggregation.

View

Fulltext

Code

TR-IIS-19-003

Subject / Author / Abstract

Calculating a backtracking algorithm: an exercise in monadic program derivation
Shin-Cheng Mu

Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively less attention has been paid to reasoning about monadic programs. In this report we derive a backtracking algorithm for problem specifications that use a monadic unfold to generate possible solutions, which are filtered using a scanl-like predicate. We develop theorems that convert a variation of scanl to a foldr that uses the state monad, as well as theorems constructing hylomorphism.

The algorithm is used to solve the n-queens puzzle, our running example. The aim is to develop theorems and patterns useful for the derivation of monadic programs, focusing on the intricate interaction between state and non-determinism.

View

Fulltext