:: Externally Programmed Machines :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received June 30, 2010 :: Copyright (c) 2010-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, FSM_1, GLIB_000, CIRCUIT2, NAT_1, ARYTM_3, XXREAL_0, MSUALG_1, TURING_1, PARTFUN1, ZFMISC_1, GRAPHSP, ARYTM_1, AMI_1, PBOOLE, EXTPRO_1, GROUP_9, COMPOS_1, MEMSTR_0, GOBRD13, QUANTAL1, FUNCT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1, PBOOLE, NUMBERS, FUNCT_7, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, NAT_1, FUNCOP_1, FUNCT_4, FINSEQ_1, FUNCT_2, DOMAIN_1, MEASURE6, STRUCT_0, XXREAL_0, MEMSTR_0, COMPOS_0, COMPOS_1; constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, FUNCT_7, GRAPH_2, RELSET_1, PRE_POLY, PBOOLE, COMPOS_1, MEMSTR_0, MEASURE6, XTUPLE_0; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, INT_1, COMPOS_1, MEMSTR_0, CARD_1, MEASURE6, COMPOS_0, NAT_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: General concepts definition let N be set; struct (Mem-Struct over N, COM-Struct) AMI-Struct over N (# carrier -> set, ZeroF -> Element of the carrier, InstructionsF -> Instructions, Object-Kind -> Function of the carrier, N, ValuesF -> ManySortedSet of N, Execution -> Action of the InstructionsF, product((the ValuesF)*the Object-Kind) #); end; reserve N for with_zero set; definition let N; func Trivial-AMI N -> strict AMI-Struct over N means :: EXTPRO_1:def 1 the carrier of it = {0} & the ZeroF of it = 0 & the InstructionsF of it = {[0,{},{}]} & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT & the Execution of it = [0,{},{}] .--> id product((N --> NAT)*(0 .--> 0)); end; registration let N; cluster Trivial-AMI N -> 1-element; end; registration let N; cluster non empty for AMI-Struct over N; end; registration let N; cluster Trivial-AMI N ->with_non-empty_values; end; registration let N; cluster with_non-empty_values 1-element for AMI-Struct over N; end; definition let N; let S be with_non-empty_values AMI-Struct over N; let I be Instruction of S, s be State of S; func Exec(I,s) -> State of S equals :: EXTPRO_1:def 2 ((the Execution of S).I).s; end; reserve N for with_zero set; definition let N; let S be with_non-empty_values AMI-Struct over N; let I be Instruction of S; attr I is halting means :: EXTPRO_1:def 3 for s being State of S holds Exec(I,s) = s; end; definition let N; let S be with_non-empty_values AMI-Struct over N; attr S is halting means :: EXTPRO_1:def 4 halt S is halting; end; registration let N; cluster Trivial-AMI N -> halting; end; registration let N; cluster halting for with_non-empty_values non empty AMI-Struct over N; end; registration let N; let S be halting with_non-empty_values AMI-Struct over N; cluster halt S -> halting; end; registration let N; let S be halting with_non-empty_values AMI-Struct over N; cluster halting for Instruction of S; end; theorem :: EXTPRO_1:1 for s being State of Trivial-AMI N, i being Instruction of Trivial-AMI N holds Exec(i,s) = s; registration let E be with_zero set; cluster Trivial-AMI E -> IC-Ins-separated; end; registration let M be with_zero set; cluster IC-Ins-separated strict trivial for non empty with_non-empty_values AMI-Struct over M; end; registration let N; cluster IC-Ins-separated halting strict for 1-element with_non-empty_values AMI-Struct over N; end; begin :: General theory reserve x,y,z,A,B for set, f,g,h for Function, i,j,k for Nat; reserve S for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, s for State of S; definition let N,S; let p be (the InstructionsF of S)-valued Function; let s be State of S; func CurInstr(p,s) -> Instruction of S equals :: EXTPRO_1:def 5 p/.IC s; end; definition let N,S; let s be State of S; let p be (the InstructionsF of S)-valued Function; func Following(p,s) -> State of S equals :: EXTPRO_1:def 6 Exec(CurInstr(p,s),s); end; definition let N,S; let p be NAT-defined (the InstructionsF of S)-valued Function; let s be State of S, k be Nat; func Comput(p,s,k) -> State of S means :: EXTPRO_1:def 7 ex f being sequence of product the_Values_of S st it = f.k & f.0 = s & for i being Nat holds f.(i+1) = Following(p,f.i); end; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be NAT-defined (the InstructionsF of S)-valued Function; let s be State of S; pred p halts_on s means :: EXTPRO_1:def 8 ex k being Nat st IC Comput(p,s,k) in dom p & CurInstr(p,Comput(p,s,k)) = halt S; end; registration let N be non empty with_zero set; let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT-defined (the InstructionsF of S)-valued Function, s be State of S; reduce Comput(p,s,0) to s; end; theorem :: EXTPRO_1:2 for N be non empty with_zero set for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT-defined (the InstructionsF of S)-valued Function, s be State of S holds Comput(p,s,0) = s; theorem :: EXTPRO_1:3 for N be non empty with_zero set for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT-defined (the InstructionsF of S)-valued Function, s be State of S, k be Nat holds Comput(p,s,k+1) = Following(p,Comput(p,s,k)); reserve N for non empty with_zero set, S for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, s for State of S; theorem :: EXTPRO_1:4 for p being NAT-defined (the InstructionsF of S)-valued Function for k holds Comput(p,s,i+k) = Comput(p,Comput(p,s,i),k); theorem :: EXTPRO_1:5 i <= j implies for N for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for p being NAT-defined (the InstructionsF of S)-valued Function for s being State of S st CurInstr(p,Comput(p,s,i)) = halt S holds Comput(p,s,j) = Comput(p,s,i); reserve n for Nat; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be NAT-defined (the InstructionsF of S)-valued Function; let s be State of S such that p halts_on s; func Result(p,s) -> State of S means :: EXTPRO_1:def 9 ex k st it = Comput(p,s,k) & CurInstr(p,it) = halt S; end; theorem :: EXTPRO_1:6 for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds Comput(P,s,k+1) = Exec(P.IC Comput(P,s,k),Comput(P,s,k)); theorem :: EXTPRO_1:7 for S being IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N for P being Instruction-Sequence of S for s being State of S, k st P.IC Comput(P,s,k) = halt S holds Result(P,s) = Comput(P,s,k); theorem :: EXTPRO_1:8 for S being IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k st P.IC Comput(P,s,k) = halt S for i holds Result(P,s) = Result(P,Comput(P,s,i)); definition let N; let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be (the InstructionsF of S)-valued NAT-defined Function; let IT be PartState of S; attr IT is p-autonomic means :: EXTPRO_1:def 10 for P,Q being Instruction-Sequence of S st p c= P & p c= Q for s1,s2 being State of S st IT c= s1 & IT c= s2 for i holds Comput(P,s1,i)|dom IT = Comput(Q,s2,i)|dom IT; end; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be (the InstructionsF of S)-valued NAT-defined Function; let IT be PartState of S; attr IT is p-halted means :: EXTPRO_1:def 11 for s being State of S st IT c= s for P being Instruction-Sequence of S st p c= P holds P halts_on s; end; registration let N; cluster halting strict for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; end; begin :: Preprograms theorem :: EXTPRO_1:9 for S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for l being Nat, I being Instruction of S for P being NAT-defined (the InstructionsF of S)-valued Function st l .--> I c= P for s being State of S st IC S .--> l c= s holds CurInstr(P,s) = I; theorem :: EXTPRO_1:10 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for l being Nat for P being NAT-defined (the InstructionsF of S)-valued Function st l .--> halt S c= P for p being l-started PartState of S holds p is P-halted; theorem :: EXTPRO_1:11 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for l being Nat for P being NAT-defined (the InstructionsF of S)-valued Function st l .--> halt S c= P for p being l-started PartState of S for s being State of S st p c= s for i holds Comput(P,s,i) = s; theorem :: EXTPRO_1:12 for S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for l being Nat for P being NAT-defined (the InstructionsF of S)-valued Function st l .--> halt S c= P for p being l-started PartState of S holds p is P-autonomic; registration let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let P be non halt-free (the InstructionsF of S)-valued NAT-defined Function; cluster P-autonomic P-halted non empty for FinPartState of S; end; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let P be non halt-free NAT-defined (the InstructionsF of S)-valued Function; mode Autonomy of P -> FinPartState of S means :: EXTPRO_1:def 12 it is P-autonomic P-halted; end; definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be non halt-free NAT-defined (the InstructionsF of S)-valued Function; let d be FinPartState of S; assume d is Autonomy of p; func Result(p,d) -> FinPartState of S means :: EXTPRO_1:def 13 for P being Instruction-Sequence of S st p c= P for s being State of S st d c= s holds it = Result(P,s)|dom d; end; begin :: Computability definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be non halt-free NAT-defined (the InstructionsF of S)-valued Function; let d be FinPartState of S, F be Function; pred p,d computes F means :: EXTPRO_1:def 14 for x being set st x in dom F ex s being FinPartState of S st x = s & d +* s is Autonomy of p & F.s c= Result(p,d+* s); end; theorem :: EXTPRO_1:13 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for p being non halt-free NAT-defined (the InstructionsF of S)-valued Function for d being FinPartState of S holds p,d computes {}; theorem :: EXTPRO_1:14 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for p being non halt-free NAT-defined (the InstructionsF of S)-valued Function for d being FinPartState of S holds d is Autonomy of p iff p,d computes {} .--> Result(p,d); theorem :: EXTPRO_1:15 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for p being non halt-free NAT-defined (the InstructionsF of S)-valued Function for d being FinPartState of S holds d is Autonomy of p iff p,d computes {} .--> {}; begin :: InsType & InsCode registration let N; cluster IC-Ins-separated for non empty AMI-Struct over N; end; begin :: Some Remarks on AMI-Struct reserve N for with_zero non empty set; theorem :: EXTPRO_1:16 for S being IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, p be NAT-defined (the InstructionsF of S)-valued Function, s being State of S holds p halts_on s iff ex i st p halts_at IC Comput(p,s,i); theorem :: EXTPRO_1:17 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p be NAT-defined (the InstructionsF of S)-valued Function, s being State of S, k being Nat st p halts_on s holds Result(p,s) = Comput(p,s,k) iff p halts_at IC Comput(p,s,k); theorem :: EXTPRO_1:18 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for P being (the InstructionsF of S)-valued NAT-defined Function, s being State of S, k st P halts_at IC Comput(P,s,k) holds Result(P,s) = Comput(P,s,k); theorem :: EXTPRO_1:19 i <= j implies for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for P being (the InstructionsF of S)-valued NAT-defined Function for s being State of S st P halts_at IC Comput(P,s,i) holds P halts_at IC Comput(P,s,j); theorem :: EXTPRO_1:20 i <= j implies for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for P being (the InstructionsF of S)-valued NAT-defined Function for s being State of S st P halts_at IC Comput(P,s,i) holds Comput(P,s,j) = Comput(P,s,i); theorem :: EXTPRO_1:21 for S being IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N for P being Instruction-Sequence of S for s being State of S st ex k st P halts_at IC Comput(P,s,k) for i holds Result(P,s) = Result(P,Comput(P,s,i)); definition let N; let S be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; let p be NAT-defined (the InstructionsF of S)-valued Function; let s be State of S such that p halts_on s; func LifeSpan(p,s) -> Nat means :: EXTPRO_1:def 15 CurInstr(p,Comput(p,s,it)) = halt S & for k being Nat st CurInstr(p,Comput(p,s,k)) = halt S holds it <= k; end; theorem :: EXTPRO_1:22 for N be non empty with_zero set, S be IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N, p being NAT-defined (the InstructionsF of S)-valued Function, s being State of S, m being Nat holds p halts_on s iff p halts_on Comput(p,s,m); reserve N for with_zero non empty set, S for IC-Ins-separated non empty AMI-Struct over N; reserve m,n for Nat; theorem :: EXTPRO_1:23 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, p being NAT-defined (the InstructionsF of S)-valued Function, s being State of S st p halts_on s holds Result(p,s) = Comput(p,s,LifeSpan(p,s)); theorem :: EXTPRO_1:24 for N be non empty with_zero set, S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P being Instruction-Sequence of S, s being State of S, k being Nat st CurInstr(P,Comput(P,s,k)) = halt S holds Comput(P,s,LifeSpan(P,s)) = Comput(P,s,k); theorem :: EXTPRO_1:25 for N be non empty with_zero set for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N for p being NAT-defined (the InstructionsF of S)-valued Function for s being State of S st LifeSpan(p,s) <= j & p halts_on s holds Comput(p,s,j) = Comput(p,s,LifeSpan(p,s)); theorem :: EXTPRO_1:26 for N being with_zero non empty set, S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, e being Nat, I being Instruction of S, t being e-started State of S, u being Instruction-Sequence of S st e .--> I c= u holds Following(u,t) = Exec(I, t); theorem :: EXTPRO_1:27 for S being halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P being Instruction-Sequence of S, s being State of S st s = Following(P,s) holds for n holds Comput(P,s,n) = s; theorem :: EXTPRO_1:28 for N being with_zero non empty set, S being IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, P being Instruction-Sequence of S, s being State of S, i being Instruction of S holds Exec(P.IC s,s).IC S = IC Following(P,s); theorem :: EXTPRO_1:29 for S being IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N for P being Instruction-Sequence of S for s being State of S holds P halts_on s iff ex k st CurInstr(P,Comput(P,s,k)) = halt S; reserve S for IC-Ins-separated halting non empty with_non-empty_values AMI-Struct over N; theorem :: EXTPRO_1:30 for F being Instruction-Sequence of S for s being State of S st ex k being Nat st F.(IC Comput(F,s,k)) = halt S holds F halts_on s; ::$CT theorem :: EXTPRO_1:32 for F being Instruction-Sequence of S for s being State of S, k being Nat holds F.(IC Comput(F,s,k)) <> halt S & F.(IC Comput(F,s,k+1)) = halt S iff LifeSpan(F,s) = k+1 & F halts_on s; theorem :: EXTPRO_1:33 for F being Instruction-Sequence of S for s being State of S, k being Nat st IC Comput(F,s,k) <> IC Comput(F,s,k+1) & F.(IC Comput(F,s,k+1)) = halt S holds LifeSpan(F,s) = k+1; theorem :: EXTPRO_1:34 for F being Instruction-Sequence of S for s being State of S, k being Nat st F halts_on Comput(F,s,k) & 0 < LifeSpan(F,Comput(F,s,k)) holds LifeSpan(F,s) = k+LifeSpan(F,Comput(F,s,k)); theorem :: EXTPRO_1:35 for F being Instruction-Sequence of S for s being State of S, k being Nat st F halts_on Comput(F,s,k) holds Result(F,Comput(F,s,k)) = Result(F,s); reserve S for halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N; reserve P for Instruction-Sequence of S; theorem :: EXTPRO_1:36 for s being State of S st P halts_on s for k being Nat st LifeSpan(P,s) <= k holds CurInstr(P, Comput(P,s,k)) = halt S;