1 theory UTM

     7 theory UTM

     2 imports Recursive Abacus UF GCD Turing_Hoare

     8 imports Recursive Abacus UF GCD Turing_Hoare

     3 begin

     9 begin

     4 

    10 

     5 section {* Wang coding of input arguments *}

    11 section {* Wang coding of input arguments *}

    18   TM is to transform the multiple input arguments of the TM being

    24   TM is to transform the multiple input arguments of the TM being

    19   simulated into Wang's coding, so that it can be consumed by the TM

    25   simulated into Wang's coding, so that it can be consumed by the TM

    20   compiled from @{text "rec_F"} as the second argument.

    26   compiled from @{text "rec_F"} as the second argument.

    21 

    27 

    22   However, this initialization TM (named @{text "t_wcode"}) can not be

    28   However, this initialization TM (named @{text "t_wcode"}) can not be

    24   recursive function takes a fixed number of input arguments, while

    30   recursive function takes a fixed number of input arguments, while

    25   @{text "t_wcode"} needs to take varying number of arguments and

    31   @{text "t_wcode"} needs to take varying number of arguments and

    26   tranform them into Wang's coding. Therefore, this section give a

    32   tranform them into Wang's coding. Therefore, this section give a

    27   direct construction of @{text "t_wcode"} with just some parts being

    33   direct construction of @{text "t_wcode"} with just some parts being

    28   obtained from recursive functions.

    34   obtained from recursive functions.