chrisjpurdy

% Turing machine runner - if the head moves off the end of the tape, it terminates.
% "halt" is the special halt state.

inBounds(CurrentPos, Tape) :-
    length(Tape, Length),
    CurrentPos >= 0,
    CurrentPos < Length.

% A rule is a tuple (CurrentState, CurrentNumber, NextNumber, NextState, MoveLeft)
runTM(Rules, Tape, CurrentState, CurrentPos, FinalTape) :-

chrisjpurdy

{-
Problem
-------
  Given a natural number n, randomly (uniformly) pick another between 1 and n inclusive.
  Repeat the process until you get to 1.
  For any given n, how many steps on average does it take to get to 1?

Solution
--------
  f(1) = 0

chrisjpurdy

{-
    This is a formalisation of the operational semantics and typing rules of L1, a 
    small language introduced in the Semantics of Programming Languages module in
    Part 1B of the Uni of Cambridge Computer Science course (2022-2023)

    The definitions and proofs could be extended to L2 and L3 as an exercise!
-}
module L1Semantics where

    open import Data.String hiding (toList)