caml-urm

A OCaml module for manipulating unlimited register machines
urm.mli (3566B)

 1 (** Unlimited register machines
 2 
 3  This module provides various types and functions for manipulating unlimited
 4  register machines (URMs). This implementation is besed on the specification
 5  provided in Ramin Naimi's URM simulator, which is in turn based on that of
 6  {i Computability, An introduction to recursive function theory } by Nigel J.
 7  Cutland. For example, the instruction set is given by:
 8 
 9  - [T(n, m)] transfers the contents of the [n]-th register to [m]-th register.
10  - [Z(n)] sets the value of the [n]-th register to zero.
11  - [S(n)] increments the value of the [n]-th register.
12  - [P(n)] decrements the value of the [n]-th register.
13  - [J(n, m, i)] jumps to the [i]-th instruction if the values of the [n]-th and
14  [m]-th coincide. The instruction count starts at 1, so [i = 1] jumps to the
15  first instruction.
16 
17  The register set, however, is a bit different. In Nigel's specification the
18  registers are indexed by natural numbers (starting from 1), while in this
19  implementation the registers are indexed by arbitrary integers. Also, in
20  Nigel's specification registers store natural numbers (starting from 0) and in
21  this implementation they store arbitrary integers. I have also added the [P]
22  instruction to help users handle negative integers.
23 
24  @see <sites.oxy.edu/rnaimi/home/URMsim.htm> URM simulator.
25  @see <doi.org/10.1017/CBO9781139171496> Computability, An introduction to
26  recursive function theory. *)
27 
28 (** The type of instructions. *)
29 type instruction =
30   | T of int * int
31   | Z of int
32   | S of int
33   | P of int
34   | J of int * int * int
35 
36 (** The type of all possible states of a URM. *)
37 type t
38 
39 (** An alias for {! t } *)
40 type machine = t
41 
42 (** Returns a machine whose register values are given by a function. *)
43 val of_registers : (int -> int) -> machine
44 
45 (** Returns a machine whose registers are given by the pairs in a list. All
46     other registers are zero initialized. *)
47 val of_list : (int * int) list -> machine
48 
49 (** [register m i] returns the value of the [i]-th register of [m]. *)
50 val register : machine -> int -> int
51 
52 (** A machine whose registers are all zeros. *)
53 val zeros : machine
54 
55 (** [exec m program] returns a machine whose register values are given by the
56     register values of
57     [m] with updates corresponding to the execution of [program].
58 
59     This function only returns when [program] actually halts. Please use {!
60     nexec } if you don't trust [program].
61 
62     @raise Invalid_argument if [program] attempts to jump to a non-positive
63     integer. *)
64 val exec : instruction array -> machine -> machine
65 
66 (** A safe version of {! exec }, where the maximum number of clock-cycles
67     allowed is controlled the first argument. Each instruction takes a single
68     clock-cycle to execute.
69 
70     [nexec n program] returns [Some _] if [program] halts in at most [n]
71     clock-cycles and [None] otherwise.
72 
73     @raise Invalid_argument if [program] attempts to jump to a non-positive
74     integer.  @raise Invalid_argument if [n] is not a positive integer. *)
75 val nexec : int -> instruction array -> machine -> machine option
76 
77 (** Exception raised when parsing fails. *)
78 exception Syntax_error of string
79 
80 (** Parse a program from a string. The syntax used by the parser is based on
81     the one used by Ramin Naimi's URM simulator, but again the register indexes
82     can be arbitrary integers.
83 
84     @see <sites.oxy.edu/rnaimi/home/URMsim.htm> URM simulator.
85 
86     @raise Syntax_error in case any syntax error is encountered, including
87     invalid syntax and jumps to invalid addresses. *)
88 val parse : string -> instruction array