Computation Software

Here we look at some software projects and theory that relate mathematics and computation. Such as:

Computation

Computation can be thought of a process that takes some input and uses it to produce some output.

This is like a mathematical function in that it always generates the same output for a given input (no side effects in Haskel parlance) so an example would be a sine function which generates the ratio of the opposite and hypotenuse for a given angle.

For computer theory we need to make this very general, a Turing machine can be looked at as either:

An acceptor - accepts a recursively enumerable set.
A generator - computes a recursive function
An algorithm - solves yes/no problems.

So the input/output could be anything including an infinite sequence.

Proof Assistants

More about mathematical proof on page here.

		Introduction
COQ		Some sites with introduction texts: Functional Programming in Coq Certified Programming with Dependant Types
Isabelle

Introduction

COQ

Some sites with introduction texts:

Isabelle

Semantics

This is concerned with 'meaning' of programs as opposed to their syntax.

Operational Semantics

The computations are modeled as a state with different types of command acting on that state.

There are two flavors of this big-step and small-step semantics,

Big-step

This tends to be a recursive process of combining the commands.

For instance, in a program we might put one command after another separated by a semicolon. So we can compose commands in a sequence defined like this:

(c1,s1) => s2		(c2,s2) => s3
(c1;c2,s1) => s3

Sequence

An assignment (assign variable 'x' to value 'a') is more complicated because we need to do something inside the state, so this is like a second level:

(x:=a,s1) => s(x=a)

Assign