On Signifiable Computability: Part II: An Axiomatization of Signifiable Computation and Debugger Theorems - Vladimir A. Kulyukin (Mathematics)
Signifiable computability aims to separate what is theoretically computable from what is computable through performable processes on computers with finite amounts of memory. Mathematical objects are signifiable in a formalism <semantics>L</semantics> on an alphabet <semantics>A</semantics> if they can be written as spatiotemporally finite texts in <semantics>L</semantics> on <semantics>A</semantics>. In a previous article, we formalized the signification and reference of real numbers and showed that data structures representable as multidimensional matrices of discretely finite real numbers are signifiable. In this investigation, we continue to formulate our theory of signifiable computability by offering an axiomatization of signifiable computation on discretely finite real numbers. The axiomatization implies an ontology of functions on discretely finite real numbers that classifies them as signifiable, signifiably computable, and signifiably partially computable. Relative to <semantics>L</semantics> and <semantics>A</semantics>, signification is performed with two formal systems: the Former <semantics><mover accent="true"><mover accent="true">F¨</mover>^</mover>A,L</semantics> that forms texts in <semantics>L</semantics> on <semantics>A</semantics> and the Transformer <semantics><mover accent="true"><mover accent="true">T¨</mover>^</mover>A,L</semantics> that transforms texts formed by <semantics><mover accent="true"><mover accent="true">F¨</mover>^</mover>A,L</semantics> into other texts in <semantics>L</semantics> on <semantics>A</semantics>. Singifiable computation is defined relative to <semantics>L</semantics> on <semantics>A</semantics> as a finite sequence of signifiable program states, the first of which is generated by <semantics><mover accent="true"><mover accent="true">F¨</mover>^</mover>A,L</semantics> and each subsequent state is deterministically obtained from the previous one by <semantics><mover accent="true"><mover accent="true">T¨</mover>^</mover>A,L</semantics>. We define a debugger function to investigate signifiable computation on finite-memory devices and to prove two theorems, which we call the Debugger Theorems. The first theorem shows that, for a singifiably partially computable function signified by a program on a finite-memory device <semantics>D</semantics>, the memory capacity of <semantics>D</semantics> is exceeded when running the program on signifiable discretely finite real numbers outside of the function’s domain. The second theorem shows that there are functions signifiably computable in general that become partially signifiably computable when signified by programs on <semantics>D</semantics> insomuch as the memory capacity of <semantics>D</semantics> can be exceeded even when the programs are executed on some signifiable discretely finite real numbers in the domains of these functions.