{ "nbformat": 4, "nbformat_minor": 0, "metadata": { "colab": { "provenance": [], "authorship_tag": "ABX9TyMEbvUO3kD2dPGrdFMmVPVs", "include_colab_link": true }, "kernelspec": { "name": "python3", "display_name": "Python 3" }, "language_info": { "name": "python" } }, "cells": [ { "cell_type": "markdown", "metadata": { "id": "view-in-github", "colab_type": "text" }, "source": [ "\"Open" ] }, { "cell_type": "markdown", "source": [ "# The T predicate\n", "\n", "\n" ], "metadata": { "id": "4v32slgLIcOy" } }, { "cell_type": "code", "source": [ "#@title\n", "import pandas as pd\n", "import numpy as np\n", "\n", "def program_checker(str):\n", " m = len(str)\n", " x1 = str[m - 1] == '#'\n", " x2 = all((str[i] == '1' or str[i] == '#') for i in range(m))\n", " x3 = (str.find('######') == -1)\n", " if (x1 and x2 and x3):\n", " flag = True\n", " else:\n", " flag = False\n", " print('The input ' + str + ' is not a valid 1# program.')\n", " print('It is not the concatenation of a sequence of instructions in the language.')\n", " print('So what you are asking for is undefined.')\n", " return (flag)\n", "\n", "def one_or_sharp_check(letter):\n", " if (letter==\"1\" or letter==\"#\"):\n", " return(True)\n", " else:\n", " return(False)\n", "\n", "def word_checker(strg):\n", " answer = all([one_or_sharp_check(x)==True for x in strg])\n", " return(answer)\n", "\n", "def input_checker(input_seq):\n", " seq = [word_checker(x) for x in input_seq]\n", " flag = all([word_checker(x) for x in input_seq])\n", " if not flag:\n", " print('The input sequence contains words with characters other than 1 and #.')\n", " print('So what you are asking for is undefined.')\n", " return(flag)\n", " \n", "class Augmented:\n", " def __init__(self, string, remainders):\n", " self.string = string\n", " self.remainders = remainders\n", "\n", "class Snapshot:\n", " def __init__(self, instr_number, regs, proceed,verbose,\n", " program_length, step_number,display_formal_snapshot,partial_trace):\n", " self.instr_number = instr_number\n", " self.regs = regs\n", " self.proceed = proceed\n", " self.verbose = verbose\n", " self.program_length = program_length\n", " self.step_number = step_number\n", " self.display_formal_snapshot = display_formal_snapshot\n", " self.partial_trace = partial_trace\n", " \n", "def preparse(xstr):\n", " b = xstr.string.find('#1')\n", " xstr.remainders = xstr.remainders + [xstr.string[:(b + 1)]]\n", " xstr.string = xstr.string[(b + 1):]\n", " return (xstr)\n", "\n", "\n", "\n", "def parse(y):\n", " tempx = Augmented(y, [])\n", " while tempx.string.find('#1') >= 0:\n", " tempx = preparse(tempx)\n", " return (tempx.remainders + [tempx.string])\n", "\n", "def unparse(p):\n", " return (''.join(p))\n", "\n", "def instruction_type(instruction):\n", " if instruction[-2:] == '1#':\n", " return ('add1')\n", " if instruction[-3:] == '1##':\n", " return ('add#')\n", " if instruction[-4:] == '1###':\n", " return ('forward')\n", " if instruction[-5:] == '1####':\n", " return ('backward')\n", " if instruction[-6:] == '1#####':\n", " return ('cases')\n", "\n", "def tail(list):\n", " return (list[1:])\n", "\n", "def one_step(p, snapshot): # p is parsed\n", " truth_value = snapshot.display_formal_snapshot\n", " i = snapshot.instr_number\n", " r = snapshot.regs\n", " instruction = p[-1 + i]\n", " if snapshot.verbose:\n", " print('Step ' + str(snapshot.step_number) + ':')\n", " print('Execute instruction ' + str(i) + ':' + \" \" +\n", " instruction_gloss(instruction,i-1) \n", " + '.')\n", " if instruction_type(instruction)=='cases':\n", " billy= len(instruction) - 5\n", " if snapshot.regs[billy-1] == \"\":\n", " print('The register is empty, so we go ahead 1 instruction.')\n", " elif snapshot.regs[billy-1][0] == \"1\":\n", " print('The first symbol in that register is 1,' +\n", " ' so we delete that symbol and go forward 2 instructions.')\n", " elif snapshot.regs[billy-1][0] == \"#\":\n", " print('The first symbol in that register is #,' +\n", " ' so we delete that symbol and go forward 3 instructions.') \n", " t = instruction_type(instruction)\n", " if t == 'add1':\n", " snapshot.instr_number = 1 + snapshot.instr_number\n", " l = len(instruction)\n", " reg = len(instruction[:(l - 1)])\n", " snapshot.regs[reg - 1] = snapshot.regs[reg - 1] + '1'\n", " if t == 'add#':\n", " snapshot.instr_number = 1 + snapshot.instr_number\n", " l = len(instruction)\n", " reg = len(instruction[:(l - 2)])\n", " snapshot.regs[reg - 1] = snapshot.regs[reg - 1] + '#'\n", " if t == 'forward':\n", " l = len(instruction)\n", " offset = len(instruction[:(l - 3)])\n", " snapshot.instr_number = offset + snapshot.instr_number\n", " if t == 'backward':\n", " l = len(instruction)\n", " offset = len(instruction[:(l - 4)])\n", " snapshot.instr_number = (-offset) + snapshot.instr_number\n", " if t == 'cases':\n", " l = len(instruction)\n", " reg = len(instruction[:(l - 5)])\n", " if snapshot.regs[reg - 1] == '':\n", " snapshot.instr_number = 1 + snapshot.instr_number\n", " elif snapshot.regs[reg - 1][0] == '1':\n", " snapshot.instr_number = 2 + snapshot.instr_number\n", " snapshot.regs[reg - 1] = tail(snapshot.regs[reg - 1])\n", " elif snapshot.regs[reg - 1][0] == '#':\n", " snapshot.instr_number = 3 + snapshot.instr_number\n", " snapshot.regs[reg - 1] = tail(snapshot.regs[reg - 1])\n", " if 0< snapshot.instr_number <= len(p):\n", " snapshot.proceed = True\n", " if snapshot.verbose == True:\n", " print_snapshot(snapshot,truth_value)\n", " else:\n", " snapshot.proceed = False\n", " return (snapshot)\n", "\n", "\n", "def number_help(instr):\n", " if instruction_type(instr) == 'add1':\n", " return (len(instr) - 1)\n", " if instruction_type(instr) == 'add#':\n", " return (len(instr) - 2)\n", " if instruction_type(instr) == 'cases':\n", " return (len(instr)-5)\n", " else:\n", " return (0)\n", "\n", "\n", "def max_register(p):\n", " return (max([number_help(instr) for instr in parse(p)]))\n", "\n", "\n", "def pad(p, register_inputs):\n", " n = len(register_inputs)\n", " m = max_register(p)\n", " extras = ['' for x in range(m - n)]\n", " bigger = register_inputs + extras\n", " return (bigger)\n", "\n", "def addones(word): ### needed to get out the formal snapshots: see print_snapshot below\n", " if word == '':\n", " return(word)\n", " else:\n", " x = word[0]\n", " y = '1'+ x\n", " z = word[1:]\n", " p = addones(z)\n", " return(y + p)\n", "\n", "def word_representation(snapshot): ### needed to get out the formal snapshots: see print_snapshot below\n", " i = snapshot.instr_number\n", " r = snapshot.regs\n", " registers = len(r)\n", " a = ones(i)\n", " b = [addones(snapshot.regs[i]) + '##' for i in range(registers)]\n", " c = \"\".join(b)\n", " return(a+ '##' + c)\n", "\n", "def print_snapshot(snap,truth_value):\n", " regdf = pd.DataFrame([[snap.regs[n]] for n in range(len(snap.regs))],columns=[\"contents\"])\n", " regdf.index = np.arange(1, len(regdf) + 1)\n", " def make_pretty(styler):\n", " styler.set_properties(**{'background-color': '#FFFFCC'})\n", " styler.set_properties(**{'text-align': 'left'})\n", " #styler.set_caption(\"at the start\")\n", " #styler.hide(axis='index')\n", " return styler\n", " display(regdf.style.pipe(make_pretty)) \n", " if truth_value == True:\n", " print()\n", " w = word_representation(snap)\n", " print('The formal snapshot is ' + w)\n", " print()\n", " snap.partial_trace = snap.partial_trace + w + '#1'\n", "\n", "\n", "def step_by_step_with_snapshots(word_prog, register_inputs):\n", " step_by_step_prelim(word_prog,register_inputs,True)\n", "\n", "def step_by_step(word_prog, register_inputs):\n", " step_by_step_prelim(word_prog, register_inputs,False)\n", "\n", "def step_by_step_prelim(word_prog, register_inputs,display_formal_snapshot):\n", " truth_value = display_formal_snapshot\n", " word_prog = word_prog.replace(\" \", \"\")\n", " register_inputs = [word.replace(\" \", \"\") for word in register_inputs]\n", " if program_checker(word_prog) and input_checker(register_inputs):\n", " print('First, here is the program:')\n", " parse_explain(word_prog)\n", " print()\n", " regs = pad(word_prog, register_inputs)\n", " prog = parse(word_prog)\n", " N = len(prog)\n", " snap = Snapshot(1, regs,True,True,N,1,truth_value,'')\n", " print('The computation starts with the register contents shown below.')\n", " print('The registers include those those which you entered as part of the input')\n", " print('and also others mentioned in the input program.')\n", " print_snapshot(snap,display_formal_snapshot)\n", " print()\n", " while 0 < snap.instr_number < N + 1:\n", " snap = one_step(prog, snap)\n", " snap.step_number = (snap.step_number) + 1\n", " if snap.instr_number <= 0:\n", " print(\n", " 'The computation has not halted properly ' +\n", " 'because the control went above instruction 1 of the program.'\n", " )\n", " elif (snap.instr_number == (N + 1)) and all(\n", " snap.regs[i] == \"\"\n", " for i in range(1, len(snap.regs))):\n", " print(\n", " 'The computation then halts properly because' +\n", " ' the control is just below the last line of the program,')\n", " print('and because all registers other than R1 are empty.')\n", " print()\n", " print_snapshot(snap,display_formal_snapshot)\n", " print('The trace is shown below:') ##\n", " print(snap.partial_trace) ##\n", " print()\n", " if snap.regs[0] == \"\":\n", " print('The output is the empty word.')\n", " else:\n", " print('The output is ' + snap.regs[0] + '.')\n", " else:\n", " print('This computation does not halt.')\n", " if snap.instr_number != N + 1:\n", " print('This is because the program has ' + str(len(prog)) +\n", " ' instructions, and control at the end is not one line ' + \n", " 'below the bottom of the program.')\n", " print()\n", " else:\n", " not_blank = [\n", " i + 1 for i in range(1, len(snap.regs))\n", " if snap.regs[i] != \"\"\n", " ]\n", " print('Here is the list of registers whose contents ' +\n", " 'are not empty at this point, other than R1:' +\n", " str(not_blank) + '.')\n", " print('The register contents at the end are shown above.')\n", "\n", "\n", "def onesharp(word_prog, register_inputs):\n", " word_prog = word_prog.replace(\" \", \"\")\n", " register_inputs = [word.replace(\" \", \"\") for word in register_inputs] \n", " if program_checker(word_prog) and input_checker(register_inputs):\n", " register_inputs = [word.replace(\" \", \"\") for word in register_inputs]\n", " regs = pad(word_prog, register_inputs)\n", " prog = parse(word_prog)\n", " N = len(prog)\n", " snap = Snapshot(1, regs,True,False, N, 1,False,'')\n", " while snap.proceed:\n", " snap = one_step(prog, snap)\n", " snap.step_number = (snap.step_number)+1\n", " if (snap.instr_number == (N + 1)) and all(\n", " snap.regs[i] == \"\" for i in range(1, len(snap.regs))):\n", " return ((snap.regs)[0])\n", " else: \n", " print(\"This is undefined.\")\n", " print(\"The register contents at the end are shown below.\")\n", " print_snapshot(snap,False)\n", " else:\n", " return('undefined')\n", "\n", "\n", "def instruction_gloss(instr,line):\n", " if instruction_type(instr) == 'add1':\n", " return ('add 1 to R' + str(len(instr) - 1))\n", " if instruction_type(instr) == 'add#':\n", " return ('add # to R' + str(len(instr) - 2))\n", " if instruction_type(instr) == 'forward':\n", " w = len(instr) - 3\n", " return ('go forward ' + str(w) + ' to instruction ' + str(w+line+1))\n", " if instruction_type(instr) == 'backward':\n", " w = len(instr) - 4\n", " return ('go backward ' + str(w) + ' to instruction ' + str(line - w+1))\n", " if instruction_type(instr) == 'cases':\n", " return ('cases on R' + str(len(instr) - 5))\n", "\n", "def expanded(gorp):\n", " pgorp = parse(gorp)\n", " wwgorp = [[pgorp[x],instruction_gloss(pgorp[x],x)] for x in range(len(pgorp))]\n", " return(wwgorp)\n", "\n", "def parse_explain(prog):\n", " df = pd.DataFrame(expanded(prog),\n", " columns=[\"instruction\", 'explanation'])\n", " df.index = np.arange(1, len(df) + 1)\n", " def make_pretty(styler):\n", " styler.set_properties(**{'background-color': '#C9DFEC'}) \n", " styler.set_properties(**{'text-align': 'left'})\n", " return styler\n", " display(df.style.pipe(make_pretty))\n", " #display(df)\n", "\n", "def ones(n):\n", " w = ['1' for i in range(n)]\n", " return(unparse(w)) \n", "\n", "clear_1 = '1#####111###11####111####'\n", "\n", "move_2_1 = '11#####111111###111###1##1111####1#111111####'\n", "\n", "copy_1_2_3 = '1#####11111111###1111###11##111##11111####11#111#11111111####111#####111111###111###1##1111####1#111111####'\n", "\n", "length = '1#####1111111###11####11#1#####111###111111####111####11#####111111###111###1##1111####1#111111####'\n", "\n", "write = '1#####111111111###11111###11#11##11##111111####11#11##111111111####11#####111111###111###1##1111####1#111111####'\n", "\n", "diag = '1#####11111111111###111111###11##111#111##111##1111111####11#111#111##1111####111#####111111###111###1##1111####1#11####11#####111111###111###1##1111####1#11####'\n", "\n", "self = '1#1##1##1##1##1##1#1#1#1#1#1#1#1#1#1#1#1##1##1##1#1#1#1#1#1#1##1##1##1#1#1##1##1#1#1#1##1#1#1#1##1##1#1#1#1##1##1#1#1#1#1#1#1#1##1##1##1##1#1#1##1#1#1#1##1#1#1#1##1##1#1#1#1#1##1##1##1##1#1#1#1##1##1##1##1##1#1#1#1#1#1#1##1##1##1#1#1#1##1##1##1#1##1##1#1#1#1#1##1##1##1##1#1##1#1#1##1##1##1##1#1#1##1##1##1##1##1#1#1#1#1#1#1##1##1##1#1#1#1##1##1##1#1##1##1#1#1#1#1##1##1##1##1#1##1#1#1##1##1##1##1#####11111111111###111111###11##111#111##111##1111111####11#111#111##1111####111#####111111###111###1##1111####1#11####11#####111111###111###1##1111####1#11####'\n", "\n", "multiply = '111##1111##11#####11111111###1111###11111##111111##11111####11111#111111#11111111####111111#####111111###111###11##1111####11#111111####111#####11111111###1111###111111##1111111##11111####111111#1111111#11111111####1111111#####111111###111###111##1111####111#111111####11111#####111111###111111111###111111#####11111111111###1111111111###111111####111111#####111111111111111###111111###11111###111111#####111###1111111111111####1###11111#####111###11####111####111111#####1111###11####111####11111#11111#####111###1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111###1#1#####11111111###1111###11111##111111##11111####11111#111111#11111111####111111#####111111###111###1##1111####1#111111####1111#####111111###111###111111##1111####111111#111111####11111#####111###111111###111111111###111111#####11111111111111111111111111111111111###11111111111111111111111111###111111111111111111111111111###111111#####11111111111111111111111###1111111111111111111111111111###111111111111111111111###111111#####111111111111111111111###111111111111111111###1111111111111111111###11111#####111###111111###111111111###111111#####11111111111###1111111111111111###111111111###111111#####1111111111111###1111111111###11111111111###111111#####111###11111111###1###1111111#111111111111111111111111111111111####1111111##11111111111111111111111111111111111####1111111#111111111111111111111####1111111##11111111111111111111111####1###1111111#####111111###111###11111##1111####11111#111111####11111#####111111###111###1111##1111####1111#111111####111#####1111111111111###1111111111###11111#111#####111111###111###11111##1111####11111#111111####1111###11111##1111111111111####11111#11111#####111111###111###111##1111####111#111111####1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111####1#####111###11####111####11#####111###11####111####111#####111###11####111####1111#####111111###111###1##1111####1#111111####'\n", "\n", "universal = '1#####1###11###11####111111#1#####111###111111###1111111###11111#####1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111###1###1####111#111111111####111##1#####1111###11###11111###111#11111#####1111111111111111111111111111111111111111111111###111111111###111##1#####1111###11###11111###111#11111#####1111111111111111111111111111111111111###111111111###111##1#####1111###11###11111###111#11111#####1111111111111111111111111111111111111111111111###111111111###111##1#####1111###11###11111###111#11111#####111111111111111111111111111111111111111111111111111111###111111111###111##1#####1111###11###11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111###111#11111#####1111111111###1###111#####111111###111###1111##1111####1111#111111####11111111111111111111111111111111111111111111111111111111111111####111#####1###11###1111###11111#1111#111111####11111##1111##111#####1111111###1111###1111##11111##11111####1111#1111111####111111111111111111111111111111111111111111111111111111111111111111111111111###111#####1###11###11111###11111#1111#111111#1111111####1111##111#####111111###111###1111##1111####1111#111111####11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111####111#####1###11###1111###1111#11111#111111####11111#11111#1111##111#####111111###111###1111##1111####1111#111111####11111#####11111111###11###1###111111#####111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111###1###1###11111111####111111#####1111###111#11111#1111####111#####111###111111#111####1#####111111###111###111##1111####111#111111####1111#####111111###111###1##1111####1#111111####111#####111111###111###1##1111####1#111111####111111111111111111111111111111111111111111111111111111111####11#####111###11111###111111111111###11##11##111111####111#11#####1###111###111##11###111#11111111111111####111##11#####11111111111111111111111111111111111111111111111111111111111111111111###1###111##11111#####1###1111111111111111111111####11111#####1111111111111111111111111111###111111111111111111111111111###11111#####111###11###111111111111111111111111111111111111111111111###11#####111111111111111111###111111111###111#11#####1###1###111#111##111##111111111111111111111111111111111111111111111111111111111###111#11#####1###111###111##11###111#111111111111111111####111#111#1111111111111111111111111111111111111111111111###11#####111111111111111111###111111111###111#11#####1###1###111##111##111##11111111111111111111111111111111111###111#11#####1###111###111##11###111#111111111111111111####111#111##111111111111111111111111###11111#####1###1###11111#####1###1###11#####11111111111111111111111###111###111##1111111111111###11#####1###11111###1###11111#111111#111111###11111#11111#111111#111111#1###11#####111111###111###111##1111####111#111111####111#####111111###111###11##1111####11#111111####1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111####11#####1###1###11#####1###1###11#####11111111111111###11###11111111###11#####1###111###1#11111111####1##1111111111####11#####111###11####111####111111#####11###11####1111#####111###11####111####'\n", "\n", "clear_2 = '11#####111###11####111####'\n", "clear_3 = '111#####111###11####111####'\n", "clear_4 = '1111#####111###11####111####'\n", "move_1_2= '1#####111111###111###11##1111####11#111111####'\n", "move_1_3= '1#####111111###111###111##1111####111#111111####'\n", "move_1_4= '1#####111111###111###1111##1111####1111#111111####'\n", "move_2_1= '11#####111111###111###1##1111####1#111111####'\n", "move_2_3= '11#####111111###111###111##1111####111#111111####'\n", "move_2_4= '11#####111111###111###1111##1111####1111#111111####'\n", "move_3_1= '111#####111111###111###1##1111####1#111111####'\n", "move_3_2= '111#####111111###111###11##1111####11#111111####'\n", "move_3_4= '111#####111111###111###1111##1111####1111#111111####'\n", "move_4_1= '1111#####111111###111###1##1111####1#111111####'\n", "move_4_2= '1111#####111111###111###11##1111####11#111111####'\n", "move_4_3= '1111#####111111###111###111##1111####111#111111####'\n", "copy_1_2_3 = '1#####11111111###1111###11##111##11111####11#111#11111111####111#####111111###111###1##1111####1#111111####'\n", "copy_1_2_4 ='1#####11111111###1111###11##1111##11111####11#1111#11111111####1111#####111111###111###1##1111####1#111111####'\n", "copy_1_3_4='1#####11111111###1111###111##1111##11111####111#1111#11111111####1111#####111111###111###1##1111####1#111111####'\n", "copy_2_3_4 = '11#####11111111###1111###111##1111##11111####111#1111#11111111####1111#####111111###111###11##1111####11#111111####'" ], "metadata": { "cellView": "form", "id": "3zbxv62sfABy" }, "execution_count": null, "outputs": [] }, { "cell_type": "markdown", "source": [ "## Snapshot and trace\n", "\n", "To start, review the definitons of *snapshot* and *trace*.\n", "\n", "##### We encode a word on {1,#}, say a1, . . . a_n by 1 a_1 1 a_2 . . . 1 a_n.\n", "That is, we put the symbol 1 between all symbols of the word that we want to encode.\n", "\n", "##### We encode a sequence of words by adding the separator ## after the enconding of each word in the sequence.\n", "\n", "#### We encode a snapshot by taking a number n and turning it into unary notation, and then following it by a sequence encoding some words. The idea is that the number n should be an instruction number in a program, and the encoded words should be the conents of the registers." ], "metadata": { "id": "oSqOVeVDIyvN" } }, { "cell_type": "markdown", "source": [ "" ], "metadata": { "id": "psrSIkk8anuG" } }, { "cell_type": "markdown", "source": [ "## New interface\n", "\n", "Here is a new interface for running program which includes a \"mode\" capability that includes the option of seeing all the snapshots and the overall trace." ], "metadata": { "id": "_zFp0Yaeas9W" } }, { "cell_type": "code", "source": [ "#title Text Register Machine
The entries for the program and registers must be words on the alphabet {1,#}, without quotes.\n", "def end_strip(list): ## removes the tail of empty registers\n", " if list == []:\n", " return(list)\n", " elif list[-1] == '':\n", " return(end_strip(list[:-1]))\n", " else:\n", " return(list)\n", "def remove_multiple_blanks(my_str):\n", " return(my_str.replace(\" \", \"\"))\n", "\n", "\n", "program = '1#' #@param {type:\"string\"}\n", "R1 = '1#1#' #@param {type:\"string\"}\n", "R2 = '' #@param {type:\"string\"}\n", "R3 = '' #@param {type:\"string\"}\n", "\n", "## For more registers, add lines here like\n", "## R4 = '' #@param {type:\"string\"}\n", "## You also must modify the definition of 'a' below accordingly.\n", "\n", "mode = 'step by step with snapshots and trace' #@param [\"output only\", \"step by step\",\"step by step with snapshots and trace\"]\n", "\n", "# First, we delete the last batch of empty registers\n", "# to simplify the output \n", "a = [R1,R2,R3]\n", "a = [remove_multiple_blanks(x) for x in a]\n", "\n", "non_empty_registers = end_strip(a)\n", "if mode == 'output only':\n", " onesharp(program,non_empty_registers)\n", "if mode == 'step by step':\n", " step_by_step(program,non_empty_registers)\n", "if mode == 'step by step with snapshots and trace':\n", " step_by_step_with_snapshots(program,non_empty_registers)" ], "metadata": { "id": "THLtJ9nHTq16", "colab": { "base_uri": "https://localhost:8080/", "height": 583 }, "outputId": "9efd98f1-5e88-4e25-fea6-b2a293091f88" }, "execution_count": null, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "First, here is the program:\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 instructionexplanation
11#add 1 to R1
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The computation starts with the register contents shown below.\n", "The registers include those those which you entered as part of the input\n", "and also others mentioned in the input program.\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 contents
11#1#
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The formal snapshot is 1##111#111###\n", "\n", "\n", "Step 1:\n", "Execute instruction 1: add 1 to R1.\n", "The computation then halts properly because the control is just below the last line of the program,\n", "and because all registers other than R1 are empty.\n", "\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 contents
11#1#1
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The formal snapshot is 11##111#111#11##\n", "\n", "The trace is shown below:\n", "1##111#111####111##111#111#11###1\n", "\n", "The output is 1#1#1.\n" ] } ] }, { "cell_type": "markdown", "source": [ "If you want to expand the interface to handle more than three registers, open the code and look around.\n", "\n", "You can also run things in the notebook cells as we have been doing it. See below for an example of how we would see the snapshots in a step_by_step execution." ], "metadata": { "id": "Jr2BwIF0JYFl" } }, { "cell_type": "code", "source": [ "#@title\n", "step_by_step_with_snapshots('1#1#',['##'])\n" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/", "height": 768 }, "id": "DRCVegtmD0b7", "outputId": "3ddf4fd8-bbbf-4546-a0c9-f1f94b640c4c" }, "execution_count": null, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "First, here is the program:\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 instructionexplanation
11#add 1 to R1
21#add 1 to R1
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The computation starts with the register contents shown below.\n", "The registers include those those which you entered as part of the input\n", "and also others mentioned in the input program.\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 contents
1##
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The formal snapshot is 1##1#1###\n", "\n", "\n", "Step 1:\n", "Execute instruction 1: add 1 to R1.\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 contents
1##1
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The formal snapshot is 11##1#1#11##\n", "\n", "Step 2:\n", "Execute instruction 2: add 1 to R1.\n", "The computation then halts properly because the control is just below the last line of the program,\n", "and because all registers other than R1 are empty.\n", "\n" ] }, { "output_type": "display_data", "data": { "text/plain": [ "" ], "text/html": [ "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
 contents
1##11
\n" ] }, "metadata": {} }, { "output_type": "stream", "name": "stdout", "text": [ "\n", "The formal snapshot is 111##1#1#1111##\n", "\n", "The trace is shown below:\n", "1##1#1####111##1#1#11###1111##1#1#1111###1\n", "\n", "The output is ##11.\n" ] } ] }, { "cell_type": "code", "source": [ "#@title\n", "step_by_step_with_snapshots(diag,['1#'])\n" ], "metadata": { "id": "PDDArRklTXkB" }, "execution_count": null, "outputs": [] }, { "cell_type": "markdown", "source": [ "### We also want to check that various relations leading up to the T predicate are computable. This part is work in progress, with the results obtained so far shown below." ], "metadata": { "id": "5QITuuDvu0XA" } }, { "cell_type": "code", "source": [ "def snapshot_check(w): ## tells True or False if the input is a snapshot\n", " index = w.index('##')\n", " front = w[:index] ## divide the string by the first occurrence of ##\n", " back = w[index:]\n", " first_truth_value = all([(x == '1') for x in front]) \n", " ## first_truth_value tells if all symbols in the front are 1\n", " j = len(back)\n", " indices_of_sharp = [(2*i) for i in range(j//2) if back[2*i]=='#']\n", " second_truth_value = all([(back[1 + i] == '#') for i in indices_of_sharp])\n", " ## the second truth value tells the separators ## are done correctly \n", " return(first_truth_value and second_truth_value)\n", "\n", "def halting_snapshot_check(p,w): \n", " ## tells True or False if the input is a snapshot\n", " # which suggests that the program p has halted properly\n", " # So we check that p is a program, \n", " # that the number at the front of w is 1 + (the number of instructions in p),\n", " # and that in w, all registers after R1 are empty\n", " parsed_p = parse(p)\n", " N = len(parsed_p)\n", " #print('N =' + str(N))\n", " index = w.index('##')\n", " front = w[:index] ## divide the string by the first occurrence of ##\n", " #print('len front = '+ str(len(front)))\n", " length_check = (N + 1 == len(front))\n", " #print(length_check)\n", " back = w[index:]\n", " first_truth_value = all([(x == '1') for x in front]) \n", " ## first_truth_value tells if all symbols in the front are 1\n", " j = len(back)\n", " indices_of_sharp = [(2*i) for i in range(j//2) if back[2*i]=='#']\n", " second_truth_value = all([(back[1 + i] == '#') for i in indices_of_sharp])\n", " ## the second truth value tells the separators ## are done correctly \n", " w2 = back[2:]\n", " #print('w2' +w2)\n", " index2 =w2.index('##') \n", " #print(index2)\n", " back2 = w2[index2:]\n", " #print(back2)\n", " emptiness_check = all(x=='#' for x in back2)\n", " #print(emptiness_check)\n", " return(first_truth_value and second_truth_value and length_check and emptiness_check)\n" ], "metadata": { "id": "6JN-Jns_GKjY" }, "execution_count": null, "outputs": [] }, { "cell_type": "code", "source": [ "snapshot_check('111##1#11#1111##')" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "0NVduL92jkIe", "outputId": "a59e7504-21aa-49d8-fd22-69171975bc8a" }, "execution_count": null, "outputs": [ { "output_type": "execute_result", "data": { "text/plain": [ "False" ] }, "metadata": {}, "execution_count": 121 } ] }, { "cell_type": "code", "source": [ "print([0,1,2,3,4,5][2:])\n", "print(parse('1#1#'))\n", "halting_snapshot_check('1#1#','111##1#1#1111##1###')" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "gLf2HFceEzzd", "outputId": "a61c88fd-73ce-4cd1-cd6b-a3424e83fb2b" }, "execution_count": null, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "[2, 3, 4, 5]\n", "['1#', '1#']\n" ] }, { "output_type": "execute_result", "data": { "text/plain": [ "False" ] }, "metadata": {}, "execution_count": 15 } ] }, { "cell_type": "markdown", "source": [ "" ], "metadata": { "id": "ZXrlT9nLazi2" } }, { "cell_type": "code", "execution_count": null, "metadata": { "id": "1zSGcVNASYpU" }, "outputs": [], "source": [ "import math\n", "\n", "def log2int(x):\n", " return(math.frexp(x)[1] - 1)\n", "\n", "def length(n):\n", " return(log2int(n+1))\n", "\n", "def index(n,m): ## this is what I write as (n)_m\n", " a = (n+1)%(2**(m+1))\n", " b = 2**m\n", " if a < b:\n", " return(0)\n", " else:\n", " return(1)\n", "\n", "def convert_numeral_to_onesharp(x):\n", " if x == 0:\n", " return('#')\n", " else:\n", " return('1') \n", "\n", "def s(n):\n", " k = length(n) \n", " s = [convert_numeral_to_onesharp(index(n,k-i-1)) for i in range(k)] \n", " t = \"\".join(s) \n", " return(t)\n", "\n", "def s_inverse(w):\n", " n = len(w)\n", " a = (2**n - 1)\n", " b = [(2** (n-i-1)) for i in range(n) if (w[i] == '1')]\n", " c = sum(b)\n", " d = c+a\n", " return(d)\n" ] }, { "cell_type": "markdown", "source": [ "We can check that ```s``` and ```s_inverse``` really are inverses." ], "metadata": { "id": "hPrmCBl2O2Fq" } }, { "cell_type": "code", "source": [ "s(s_inverse('##111##1'))" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/", "height": 35 }, "id": "aZmEUM3bMfbB", "outputId": "c379f40b-07d2-4a8b-e6c2-c6b28db6e002" }, "execution_count": null, "outputs": [ { "output_type": "execute_result", "data": { "text/plain": [ "'##111##1'" ], "application/vnd.google.colaboratory.intrinsic+json": { "type": "string" } }, "metadata": {}, "execution_count": 20 } ] }, { "cell_type": "code", "source": [ "s_inverse(s(4234))" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "V7ZdL2VlOwg-", "outputId": "8af90054-1abb-44b5-b0ea-d782db870723" }, "execution_count": null, "outputs": [ { "output_type": "execute_result", "data": { "text/plain": [ "4234" ] }, "metadata": {}, "execution_count": 21 } ] }, { "cell_type": "code", "source": [ "for n in range(256):\n", " print((n,s(n), s_inverse(s(n))))\n", " " ], "metadata": { "id": "UCmVDOcndqdN" }, "execution_count": null, "outputs": [] }, { "cell_type": "code", "source": [ "s(55)" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/", "height": 35 }, "id": "qZnud4B1SZdp", "outputId": "4988e9ec-ff84-4f67-f19d-61f37863c656" }, "execution_count": null, "outputs": [ { "output_type": "execute_result", "data": { "text/plain": [ "'11###'" ], "application/vnd.google.colaboratory.intrinsic+json": { "type": "string" } }, "metadata": {}, "execution_count": 23 } ] }, { "cell_type": "code", "source": [ "a = ['1#','','1','','']\n", "first_index = a.index('')\n", "reversed_list = a[::-1]\n", "first_index_in_reversed = reversed_list.index('')\n", "last_index = len(a) -1 - first_index_in_reversed\n", "last_index\n", "print(a[:last_index-1])" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "bWbLxZVmFSkS", "outputId": "ed7d6ad1-fd3c-40f9-e850-90de9450a605" }, "execution_count": null, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "['1#', '', '1']\n" ] } ] }, { "cell_type": "code", "source": [ "a = ['1#1#', '11', '','#','']\n", "print(a)\n", "first_index = a.index('')\n", "reversed_list = a[::-1]\n", "print(reversed_list)\n", "first_index_in_reversed = reversed_list.index('')\n", "last_index = len(a) -1 - first_index_in_reversed\n", "print(last_index)\n", "non_empty_registers = a[:last_index]\n", "print(non_empty_registers)" ], "metadata": { "colab": { "base_uri": "https://localhost:8080/" }, "id": "2_v48hnPqnnn", "outputId": "229605e1-8baa-401b-b433-39887e727e36" }, "execution_count": null, "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "['1#1#', '11', '', '#', '']\n", "['', '#', '', '11', '1#1#']\n", "4\n", "['1#1#', '11', '', '#']\n" ] } ] } ] }