大數學 维基
Advertisement

這是提交給日本大數競賽我的日語博客文章的中文翻譯。

我用編程語言Qp實施了漢堡包表記。編程語言Qp的源代碼会自動轉換為自然語言。


源代碼


  // ハンバーガーとパティの型の基底となる整数の列の入れ子の型NestedArrayの定義
  NEST( NestedArray , int );

  // NestedArray型の変数sの宣言
  USE( NestedArray , s );

  // ハンバーガーであることを表す関係IsHamburgerの宣言
  IMP( bool , IsHamburger , s );
  ROMANISE( IsHamburger );
  SET( IsHamburger , SEPARATOR , LBRACE , RBRACE + SYMBOLISE( IsHamburger ) );

  // パティであることを表す関係の宣言
  IMP( bool , IsPatty , s );
  ROMANISE( IsPatty );
  SET( IsPatty , SEPARATOR , LBRACE , RBRACE + SYMBOLISE( IsPatty ) );

  // IsHamburgerの定義
  // ハンバーガーは1個以上のパティの列
  DEF( IsHamburger ){

    // 列ではなく単に整数の場合はハンバーガーでない
    // 整数(列でないので長さが未定義)と、整数の長さ1の列は区別される
    IF( DENESTABLE( s ) , RETURN( false ) ) ,
      // 空列はハンバーガーでない
      IF( LENGTH( s ) == 0 , RETURN( false ) ) ,
      // 0項目がパティか否かを判定
      IF( ! IsPatty( ENTRY( s , 0 ) ) , RETURN( false ) ) ,
      IF( LENGTH( s ) == 1 , RETURN( true ) ) ,
      // 0項目以降がパティの列であるかを判定
      RETURN( IsHamburger( FINSEG( s , LENGTH( s ) - 1 ) ) )

      };
  
  // NestedArray型の変数を文字列に変換する関数ToStringの宣言
  IMP( string , ToString , s );
  ROMANISE( ToString );
  
  // string型の変数c0,c1の宣言
  USE( string , c0 );
  USE( string , c1 );

  // ToStringの定義
  DEF( ToString ){

    IF( IsHamburger( s ) ,
	// 0項目のパティを変換した文字列をc0と置く
	PUT( c0 , ToString( ENTRY( s , 0 ) ) ) ,
	IF( LENGTH( s ) == 1 , RETURN( "(" + c0 + "]" ) ) ,
	// 0項目以降のパティからなるハンバーガーを変換した文字列をc1と置く
	PUT( c1 , ToString( FINSEG( s, LENGTH( s ) - 1 ) ) ) ,
	RETURN( "(" + c0 + "|" + FINSEG( c1 , LENGTH( c1 ) - 1 ) )
	
	) ,
      IF( IsPatty( s ) ,
	  IF( LENGTH( s ) == 0 , RETURN( "肉" ) ) ,
	  // 0項目のハンバーガーを変換した文字列をc0と置く
	  PUT( c0 , ToString( ENTRY( s , 0 ) ) ) ,
	  // 0項目以降のハンバーガーからなるパティを変換した文字列をc1と置く
	  PUT( c1 , ToString( FINSEG( s, LENGTH( s ) - 1 ) ) ) ,
	  RETURN( "肉" + c0 + "肉" + FINSEG( c1 , LENGTH( c1 ) - 1 ) )
	  ) ,
      // ハンバーガーでもパティでもない場合は例外を投げる
      EXIT

      };

  // InspectをToStringのaliasとする
  // オリジナルに合わせて導入したが、これはどこで使うのだろうか
#define Inspect( VARIABLE ) ToString( VARIABLE )

  // NestedArray型の変数tの宣言
  USE( NestedArray , t );
  
  // NestedArrayの大小関係IsLessThanの宣言
  IMP( bool , IsLessThan , s , t );
  ROMANISE( IsLessThan );
  SET( IsLessThan , SEPARATOR , SPACE , STR( < ) , SPACE );

  // IsLessThanの定義
  DEF( IsLessThan ){

    IF( IsHamburger( s ) && IsHamburger( t ) ,
	IF( LENGTH( t ) == 1 , RETURN( IsLessThan( ENTRY( s , 0 ) , ENTRY( t , 0 ) ) ) ) ,
	IF( LENGTH( s ) == 1 , RETURN( ! IsLessThan( ENTRY( t , 0 ) , ENTRY( s , 0 ) ) ) ) ,
	IF( ENTRY( s , 0 ) == ENTRY( t , 0 ) , RETURN( IsLessThan( FINSEG( s , LENGTH( s ) - 1 ) , FINSEG( t , LENGTH( t ) - 1 ) ) ) ) ,
	RETURN( IsLessThan( ENTRY( s , 0 ) , ENTRY( t , 0 ) ) )
	) ,
      IF( IsPatty( s ) && IsPatty( t ) ,
	  IF( LENGTH( t ) == 0 , RETURN( false ) ) ,
	  IF( LENGTH( s ) == 0 , RETURN( true ) ) ,
	  IF( LENGTH( t ) == 1 , RETURN( LENGTH( s ) == 1 && IsLessThan( ENTRY( s , 0 ) , ENTRY( t , 0 ) ) ) ) ,
	  IF( LENGTH( s ) == 1 , RETURN( true ) ) ,
	  IF( IsLessThan( ENTRY( s , 0 ) , ENTRY( t , 0 ) ) , RETURN( true ) ) ,
	  IF( IsLessThan( ENTRY( t , 0 ) , ENTRY( s , 0 ) ) , RETURN( false ) ) ,
	  IF( IsLessThan( ENTRY( s , 1 ) , ENTRY( t , 1 ) ) , RETURN( true ) ) ,
	  IF( IsLessThan( ENTRY( t , 1 ) , ENTRY( s , 1 ) ) , RETURN( false ) ) ,
	  RETURN( IsLessThan( FINSEG( s , LENGTH( s ) - 2 ) , FINSEG( t , LENGTH( t ) - 2 ) ) )
	  ) ,
      // ハンバーガー同士でもパティ同士でもない場合は例外を投げる
      EXIT
      
      };
  
  // ハンバーガーがパティ基準でバランスがよいことを表す関係IsBalancedForの宣言
  IMP( bool , IsBalancedFor , s , t );
  ROMANISE( IsBalancedFor );
  SET( IsBalancedFor , SEPARATOR , LPAREN , RPAREN + SYMBOLISE( IsBalancedFor ) + LPAREN , RPAREN );

  // パティをオッドパティとパティ素材に切り分ける関数OddPattyOfとPattyMaterialOfの宣言
  IMP( NestedArray , OddPattyOf , s );
  IMP( NestedArray , PattyMaterialOf , s );
  ROMANISE( OddPattyOf );
  ROMANISE( PattyMaterialOf );

  // より技巧的であることを表す関係IsLessTechnicalThanの宣言
  IMP( bool , IsLessTechnicalThan , s , t );
  ROMANISE( IsLessTechnicalThan );
  SET( IsLessTechnicalThan , SEPARATOR , LPAREN , RPAREN + SYMBOLISE( IsLessTechnicalThan ) + LPAREN , RPAREN );
  
  // パティ1個からハンバーガーを構成する関数マクロとハンバーガー1個からパティを構成する関数マクロを導入
  // どちらもカッコに入れるだけの関数NWRAPを用いた同じ関数マクロだが意図を明確にするためだけに2つの名前をつける
#define Hamburger( PATTY ) NWRAP( PATTY ) 
#define Patty( HAMBURGER ) NWRAP( HAMBURGER ) 

  // NestedArray型の変数u0の宣言
  USE( NestedArray , u0 );

  // IsBalancedForの定義
  DEF( IsBalancedFor ){

    IF( ! IsHamburger( s ) || ! IsPatty( t ) , EXIT ) ,
      IF( LENGTH( t ) == 0 , RETURN( false ) ) ,
      IF( LENGTH( s ) == 1 ,
	  IF( LENGTH( ENTRY( s , 0 ) ) == 0 , RETURN( true ) ) ,
	  // スパゲティはハンバーガーの具材に入らない
	  IF( ! IsBalancedFor( Hamburger( OddPattyOf( ENTRY( s , 0 ) ) ) , t ) , RETURN( false ) ) ,
	  // sの唯一のパティのパティ素材をu0と置く
	  PUT( u0 , PattyMaterialOf( ENTRY( s , 0 ) ) ) ,
	  // パティ素材をパティの列として実装したのでu0にカッコは不要である
	  IF( ! IsLessTechnicalThan( u0 , t ) && IsLessThan( Hamburger( OddPattyOf( t ) ) , s ) , RETURN( false ) ) ,
	  IF( ! IsBalancedFor( ENTRY( u0 , 0 ) , t ) , RETURN( false ) ) ,
	  IF( LENGTH( u0 ) == 1 , RETURN( true ) ) ,
	  RETURN( IsBalancedFor( ENTRY( u0 , 1 ) , t ) )
	  ) ,
      IF( ! IsBalancedFor( INISEG( s , LENGTH( s ) - 1 ) , t ) , RETURN( false ) ) ,
      RETURN( IsBalancedFor( Hamburger( ENTRY( s , LENGTH( s ) - 1 ) ) , t ) )
      
      };
  
  // ハンバーガーの食べやすさを表す関係IsEasyToEatの宣言
  IMP( bool , IsEasyToEat , s );
  ROMANISE( IsEasyToEat );
  SET( IsEasyToEat , SEPARATOR , LPAREN , RPAREN + SYMBOLISE( IsEasyToEat ) );

  // NestedArray型の変数u1の宣言
  USE( NestedArray , u1 );

  // IsEasyToEatの定義
  DEF( IsEasyToEat ){

    IF( ! IsHamburger( s ) , EXIT ) ,
      IF( LENGTH( s ) == 1 ,
	  IF( LENGTH( ENTRY( s , 0 ) ) == 0 , RETURN( true ) ) ,
	  PUT( u0 , OddPattyOf( ENTRY( s , 0 ) ) ) ,
	  PUT( u1 , PattyMaterialOf( ENTRY( s , 0 ) ) ) ,
	  // スパゲティはハンバーガーの具材に入らない
	  IF( ! IsEasyToEat( Hamburger( u0 ) ) , RETURN( false ) ) ,
	  IF( LENGTH( u1 ) == 2 && LENGTH( u0 ) % 2 == 0 && LENGTH( u0 ) >= 2 ,
	      IF( ! IsLessThan( ENTRY( u0 , LENGTH( u0 ) - 2 ) , ENTRY( u1 , 0 ) ) , RETURN( false ) )
	      ) ,
	  IF( ! IsEasyToEat( ENTRY( u1 , 0 ) ) , RETURN( false ) ) ,
	  IF( LENGTH( u1 ) == 1 , RETURN( IsBalancedFor( ENTRY( u1 , 0 ) , ENTRY( s , 0 ) ) ) ) ,
	  IF( ! IsEasyToEat( ENTRY( u1 , 1 ) ) , RETURN( false ) ) ,
	  RETURN( IsBalancedFor( ENTRY( u1 , 1 ) , ENTRY( s , 0 ) ) )
	  ) ,
      IF( LENGTH( s ) == 2 ,
	  IF( ! IsEasyToEat( ENTRY( s , 0 ) ) , RETURN( false ) ) ,
	  IF( ! IsEasyToEat( ENTRY( s , 1 ) ) , RETURN( false ) ) ,
	  RETURN( ! IsLessThan( ENTRY( s , 0 ) , ENTRY( s , 1 ) ) )
	  ) ,
      IF( ! IsEasyToEat( INISEG( s , LENGTH( s ) - 1 ) ) , RETURN( false ) ) ,
      RETURN( IsEasyToEat( Hamburger( ENTRY( s , LENGTH( s ) - 2 ) ) + Hamburger( ENTRY( s , LENGTH( s ) - 1 ) ) ) )
      
      };


  // 肉の枚数を返す関数NumberOfMeatInの宣言
  IMP( nat , NumberOfMeatIn , s );
  ROMANISE( NumberOfMeatIn );

  // NumberOfMeatInの定義
  // Rubyと違って文字列の肉をカウントする機能はないので愚直に数える
  DEF( NumberOfMeatIn ){

    IF( IsHamburger( s ) ,
	IF( LENGTH( s ) == 1 , RETURN( NumberOfMeatIn( ENTRY( s , 0 ) ) ) ) ,
	RETURN( NumberOfMeatIn( ENTRY( s , 0 ) ) + NumberOfMeatIn( FINSEG( s , LENGTH( s ) - 1 ) ) )
	) ,
      IF( IsPatty( s ) ,
	  IF( LENGTH( s ) == 0 , RETURN( 1 ) ) ,
	  RETURN( 1 + NumberOfMeatIn( ENTRY( s , 0 ) ) + NumberOfMeatIn( FINSEG( s , LENGTH( s ) - 1  ) ) )
	  ) ,
      EXIT

      };
  
  // nat型の変数nとmの宣言
  USE( nat , n );
  USE( nat , m );

  // 基本列を返す関数Expandとその補助関数Expand_Bodyの宣言
  IMP( NestedArray , Expand , s , n );
  IMP( NestedArray , Expand_Body , s , n , t , m );
  ROMANISE( Expand );
  ROMANISE( Expand_Body );
  SET( Expand , SEPARATOR , SPACE , LBRACK , RBRACK );

  // 限界の表記を返す関数Lambdaの宣言
  IMP( NestedArray , Lambda , n );
  SET( Lambda , SYMBOL , STR( \\Lambda ) );

  // Expandの定義
  // Qpにforループやwhileループはないので、補助関数の再帰でループを回す
  // 便宜上最小のハンバーガーLambda( 0 )を入れて開始
  DEF( Expand ){ RETURN( Expand_Body( s , NumberOfMeatIn( s ) + n , Lambda( 0 ) , 1 ) ) };

  // 正整数をハンバーガーにパースする関数ParseToHamburgerとその補助関数ParseToHamburger_Bodyの宣言
  IMP( NestedArray , ParseToHamburger , n );
  IMP( NestedArray , ParseToHamburger_Body , n , m );
  ROMANISE( ParseToHamburger );
  ROMANISE( ParseToHamburger_Body );
  
  // Expand_Bodyの定義
  // 3^n以下の正整数を探索し、tより大きくかつs未満かつ肉の枚数がn以下の食べやすいハンバーガーにパースされる正整数を見付けるたびにtをそのハンバーガーに更新する
  DEF( Expand_Body ){

    IF( ! IsHamburger( s ) || ! IsHamburger( t ) , EXIT ) ,
      IF( m > ( 3 ^ n ) , RETURN( t ) ) ,
      PUT( u0 , ParseToHamburger( m ) ) ,
      IF( IsHamburger( u0 ) ,
	  IF( IsLessThan( t , u0 ) &&
	      IsLessThan( u0 , s ) &&
	      NumberOfMeatIn( u0 ) <= n &&
	      IsEasyToEat( u0 ) ,
	      RETURN( Expand_Body( s , n , u0 , m + 1 ) )
	      )
	  ),
      RETURN( Expand_Body( s , n , t , m + 1 ) )
    
      };
  
  // ParseToHamburgerの定義
  DEF( ParseToHamburger ){

    // 3進数展開の各桁0,1,2を(,|,]に対応させる
    // 右端が]でないものはハンバーガーですらない-1にパースする
    IF( n % 3 != 2 , RETURN( ENNEST( -1 ) ) ) ,
      // 右端を除去して補助関数でループする
      // 3進数展開の性質上左端は(でないが、左端の左に(が適量並んでいる扱いとする実装を行うため、右端のみ除去する
      RETURN( ParseToHamburger_Body( n / 3 , 0 ) )
    
      };

  // 正整数をパティにパースする関数ParseToPattyとその補助関数ParseToPatty_Bodyの宣言
  IMP( NestedArray , ParseToPatty , n );
  IMP( NestedArray , ParseToPatty_Body , n , m );
  ROMANISE( ParseToPatty );
  ROMANISE( ParseToPatty_Body );

  // ParseToHamburger_Bodyの定義
  // mは参照中の桁数-1
  DEF( ParseToHamburger_Body ){

    // |が見付からなかった場合はパティにパースしてハンバーガーにする
    IF( n < ( 3 ^ m ) , RETURN( Hamburger( ParseToPatty( n ) ) ) ) ,
      // m+1桁目が|でありかつm桁目までがパティにパースされる場合に、そのパティをm+2桁目以降のパース結果に挿入する
      IF( ( ( n / ( 3 ^ m ) ) % 3 ) == 1 ,
	  PUT( u0 , ParseToPatty( n % ( 3 ^ m ) ) ) ,
	  IF( IsPatty( u0 ) , RETURN( ParseToHamburger_Body( n / ( 3 ^ ( m + 1 ) ) , 0 ) + Hamburger( u0 ) ) )
	  ) ,
      // そうでない場合はmを更新する
      RETURN( ParseToHamburger_Body( n , m + 1 ) )

      };
  
  // ハンバーガーを食べ切るまでに肉を食べた枚数を数える関数Eatとその補助関数Eat_Bodyの宣言
  IMP( nat , Eat , s );
  IMP( nat , Eat_Body , s , n );
  ROMANISE( Eat );
  ROMANISE( Eat_Body );

  // Eatの定義
  DEF( Eat ){ RETURN( Eat_Body( s , 0 ) ) };

  // Eat_Bodyの定義
  // Qpはforループやwhileループを持たない代わりに、自分を再帰的に呼び出すのである!
  DEF( Eat_Body ){
    
    IF( s == Lambda( 0 ) , RETURN( n + 1 ) ) ,
      RETURN( Eat_Body( Expand( s , n + 1 ) , n + 1 ) )

      };

  // 空列の糖衣構文EmptyPattyの導入
  // ただし空列を直接返す関数は返り値の型が曖昧であるためQpには用意されていないので、代わりに-1のみからなる長さ1の列(-1)の長さ0の始切片を取って空列()を作る
  SUGAR( EmptyPatty , INISEG( Patty( ENNEST( -1 ) ) , 0 ) );
  
  // Lambdaの定義
  DEF( Lambda ){

    IF( n == 0 , RETURN( Hamburger( EmptyPatty ) ) ) ,
      PUT( u0 , Patty( Lambda( n - 1 ) ) ) ,
      RETURN( Hamburger( u0 + u0 ) )
      };

  // IsPattyの定義
  // パティは0個以上のハンバーガーの列
  DEF( IsPatty ){

    // 列ではなく単に整数の場合はハンバーガーでない
    // 整数(列でないので長さが未定義)と、整数の長さ1の列は区別される
    IF( DENESTABLE( s ) , RETURN( false ) ) ,
      IF( LENGTH( s ) == 0 , RETURN( true ) ) ,
      IF( ! IsHamburger( ENTRY( s , 0 ) ) , RETURN( false ) ) ,
      // 0項目以降がハンバーガーの列であるかを判定
      RETURN( IsPatty( FINSEG( s , LENGTH( s ) - 1 ) ) )

      };

  // odd?とeven?は使われていないようだったので実装は割愛
  
  // OddPattyOfの定義
  DEF( OddPattyOf ){

    // 肉が入力された場合は便宜上、パティですらない-1を返す
    IF( LENGTH( s ) == 0 , RETURN( ENNEST( -1 ) ) ) ,
      IF( LENGTH( s ) <= 2 , RETURN( EmptyPatty ) ) ,
      RETURN( INISEG( s , 2 ) + OddPattyOf( FINSEG( s , LENGTH( s ) - 2 ) ) )
      
      };

  // PattyMaterialOfの定義
  DEF( PattyMaterialOf ){

    // 配列ですらないものが入力された場合は例外を投げる
    IF( DENESTABLE( s ) , EXIT ) ,
      // 肉が入力された場合は便宜上、パティですらない-1を返す
      IF( LENGTH( s ) == 0 , RETURN( ENNEST( -1 ) ) ) ,
      IF( LENGTH( s ) <= 2 , RETURN( s ) ) ,
      RETURN( PattyMaterialOf( FINSEG( s , LENGTH( s ) - 2 ) ) )

      };

  // パティ素材の土台を返す関数BaseOfの宣言
  IMP( NestedArray , BaseOf , s );
  ROMANISE( BaseOf );

  // パティ素材がパティの素材であることを表す関係IsIncludedInの宣言
  IMP( bool , IsIncludedIn , s , t );
  ROMANISE( IsIncludedIn );
  SET( IsIncludedIn , SEPARATOR , LPAREN , RPAREN + SYMBOLISE( IsIncludedIn ) + LPAREN , RPAREN );

  // IsLessTechnicalThanの定義
  DEF( IsLessTechnicalThan ){

    // パティですらないものが入力された場合は例外を投げる
    // パティ素材はパティとして実装されている
    IF( ! IsPatty( s ) || ! IsPatty( t ) , EXIT ) ,
      IF( LENGTH( s ) == 0 , EXIT ) ,
      IF( LENGTH( t ) == 0 , RETURN( false ) ) ,
      // Rubyと違って[-1]のようなアクセスはできない
      RETURN( IsLessThan( BaseOf( s ) , BaseOf( PattyMaterialOf( t ) ) ) && IsIncludedIn( s , OddPattyOf( t ) ) )
      
      };

  // BaseOfの定義
  DEF( BaseOf ){

    // パティですらないものが入力された場合は例外を投げる
    IF( ! IsPatty( s ) , EXIT ) ,
      // 空列が入力された場合は例外を投げる
      IF( LENGTH( s ) == 0 , EXIT ) ,
      RETURN( ENTRY( s , LENGTH( s ) - 1 ) )

      };

  // IsIncludedInの定義
  DEF( IsIncludedIn ){

    // パティですらないものが入力された場合は例外を投げる
    // パティ素材はパティとして実装されている
    IF( ! IsPatty( s ) || ! IsPatty( t ) , EXIT ) ,
      IF( LENGTH( t ) == 0 , RETURN( false ) ) ,
      IF( LENGTH( t ) <= 2 , RETURN( s == t ) ) ,
      RETURN( IsIncludedIn( s , FINSEG( t , LENGTH( t ) - 2 ) ) )

      };

  // ParseToPattyの定義
  DEF( ParseToPatty ){

    // 3進数展開の各桁0,1,2を(,|,]に対応させる
    // 右端が]でないものはパティですらない-1にパースする
    IF( n % 3 != 2 , RETURN( ENNEST( -1 ) ) ) ,
      // 右端を除去して補助関数でループする
      // 3進数展開の性質上左端は(でないが、左端の左に(が適量並んでいる扱いとする実装を行うため、右端のみ除去する
      RETURN( ParseToPatty_Body( n / 3 , 0 ) )
      
      };
  
  // ParseToPatty_Bodyの定義
  // mは参照中の桁数-1
  DEF( ParseToPatty_Body ){

    // (が見付からなかった場合はハンバーガーにパースしてパティにする
    IF( n < ( 3 ^ m ) , RETURN( Patty( ParseToHamburger( n ) ) ) ) ,
      // m+1桁目が(でありかつm+1桁目までがハンバーガーにパースされる場合に、そのハンバーガーをm+2桁目以降のパース結果に挿入する
      IF( ( ( n / ( 3 ^ m ) ) % 3 ) == 1 ,
	  PUT( u0 , ParseToHamburger( n % ( 3 ^ ( m + 1 ) ) ) ) ,
	  IF( IsHamburger( u0 ) , RETURN( ParseToPatty_Body( n / ( 3 ^ ( m + 1 ) ) , 0 ) + Patty( u0 ) ) )
	  ) ,
      // そうでない場合はmを更新する
      RETURN( ParseToPatty_Body( n , m + 1 ) )

      };

  // デバッグ用の処理も一応実装しておく
  DISPLAY( ParseToHamburger( 22 ) , JAPANESE );


自動轉換為漢語

我將集合\(\mathbb{Z}^{\omega^{\omega}}\)定義用遞歸方法如下:

  1. 對于任意\(x \in \mathbb{Z}\), \(x \in \mathbb{Z}^{\omega^{\omega}}\)成立。
  2. 對于任意非負整數\(n\)和\(x_1,\ldots,x_n \in \mathbb{Z}^{\omega^{\omega}}\), \((x_1,\ldots,x_n) \in \mathbb{Z}^{\omega^{\omega}}\)成立。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsHamburger} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ s & \mapsto & (s)\textrm{IsHamburger} \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(s\), 則定義\((s)\textrm{IsHamburger} := \perp\)。
  2. 如果\(\textrm{Lng}(s) = 0\), 則定義\((s)\textrm{IsHamburger} := \perp\)。
  3. 如果「\(((s)_{0})\textrm{IsPatty}\)不成立」, 則定義\((s)\textrm{IsHamburger} := \perp\)。
  4. 如果\(\textrm{Lng}(s) = 1\), 則定義\((s)\textrm{IsHamburger} := \top\)。
  5. 定義\((s)\textrm{IsHamburger} := (\textrm{FinSeg}(s,\textrm{Lng}(s) - 1))\textrm{IsHamburger}\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsPatty} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ s & \mapsto & (s)\textrm{IsPatty} \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(s\), 則定義\((s)\textrm{IsPatty} := \perp\)。
  2. 如果\(\textrm{Lng}(s) = 0\), 則定義\((s)\textrm{IsPatty} := \top\)。
  3. 如果「\(((s)_{0})\textrm{IsHamburger}\)不成立」, 則定義\((s)\textrm{IsPatty} := \perp\)。
  4. 定義\((s)\textrm{IsPatty} := (\textrm{FinSeg}(s,\textrm{Lng}(s) - 1))\textrm{IsPatty}\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{ToString} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \textrm{String} \\ s & \mapsto & \textrm{ToString}( s ) \end{eqnarray*} 用遞歸方法如下:

  1. 設想\((s)\textrm{IsHamburger}\)成立。
    1. 令\(c0 := \textrm{ToString}( (s)_{0} ) \in \textrm{String}\)。
    2. 如果\(\textrm{Lng}(s) = 1\), 則定義\(\textrm{ToString}( s ) := \textrm{(} \frown c0 \frown \textrm{]}\)。
    3. 令\(c1 := \textrm{ToString}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 1) ) \in \textrm{String}\)。
    4. 定義\(\textrm{ToString}( s ) := \textrm{(} \frown c0 \frown \textrm{|} \frown \textrm{FinSeg}(c1,\textrm{Lng}(c1) - 1)\)。
  2. 設想\((s)\textrm{IsPatty}\)成立。
    1. 如果\(\textrm{Lng}(s) = 0\), 則定義\(\textrm{ToString}( s ) := \textrm{肉}\)。
    2. 令\(c0 := \textrm{ToString}( (s)_{0} ) \in \textrm{String}\)。
    3. 令\(c1 := \textrm{ToString}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 1) ) \in \textrm{String}\)。
    4. 定義\(\textrm{ToString}( s ) := \textrm{肉} \frown c0 \frown \textrm{肉} \frown \textrm{FinSeg}(c1,\textrm{Lng}(c1) - 1)\)。
  3. \(\textrm{ToString}( s )\)未定義。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsLessThan} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ ( s , t ) & \mapsto & s<t \end{eqnarray*} 用遞歸方法如下:

  1. 設想「\((s)\textrm{IsHamburger}\)和\((t)\textrm{IsHamburger}\)」成立。
    1. 如果\(\textrm{Lng}(t) = 1\), 則定義\( s<t := (s)_{0}<(t)_{0} \)。
    2. 如果\(\textrm{Lng}(s) = 1\), 則定義\( s<t := \neg( (t)_{0}<(s)_{0} )\)。
    3. 如果\((s)_{0} = (t)_{0}\), 則定義\( s<t := \textrm{FinSeg}(s,\textrm{Lng}(s) - 1)<\textrm{FinSeg}(t,\textrm{Lng}(t) - 1) \)。
    4. 定義\( s<t := (s)_{0}<(t)_{0} \)。
  2. 設想「\((s)\textrm{IsPatty}\)和\((t)\textrm{IsPatty}\)」成立。
    1. 如果\(\textrm{Lng}(t) = 0\), 則定義\( s<t := \perp\)。
    2. 如果\(\textrm{Lng}(s) = 0\), 則定義\( s<t := \top\)。
    3. 如果\(\textrm{Lng}(t) = 1\), 則定義\( s<t := \textrm{Lng}(s) = 1 \land (s)_{0}<(t)_{0} \)。
    4. 如果\(\textrm{Lng}(s) = 1\), 則定義\( s<t := \top\)。
    5. 如果\( (s)_{0}<(t)_{0} \), 則定義\( s<t := \top\)。
    6. 如果\( (t)_{0}<(s)_{0} \), 則定義\( s<t := \perp\)。
    7. 如果\( (s)_{1}<(t)_{1} \), 則定義\( s<t := \top\)。
    8. 如果\( (t)_{1}<(s)_{1} \), 則定義\( s<t := \perp\)。
    9. 定義\( s<t := \textrm{FinSeg}(s,\textrm{Lng}(s) - 2)<\textrm{FinSeg}(t,\textrm{Lng}(t) - 2) \)。
  3. \( s<t \)未定義。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsBalancedFor} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ ( s , t ) & \mapsto & (s)\textrm{IsBalancedFor}(t) \end{eqnarray*} 用遞歸方法如下:

  1. 如果「「\((s)\textrm{IsHamburger}\)不成立」或「\((t)\textrm{IsPatty}\)不成立」」, 則\((s)\textrm{IsBalancedFor}(t)\)未定義。
  2. 如果\(\textrm{Lng}(t) = 0\), 則定義\((s)\textrm{IsBalancedFor}(t) := \perp\)。
  3. 設想\(\textrm{Lng}(s) = 1\)成立。
    1. 如果\(\textrm{Lng}((s)_{0}) = 0\), 則定義\((s)\textrm{IsBalancedFor}(t) := \top\)。
    2. 如果「\(((\textrm{OddPattyOf}( (s)_{0} )))\textrm{IsBalancedFor}(t)\)不成立」, 則定義\((s)\textrm{IsBalancedFor}(t) := \perp\)。
    3. 令\(u0 := \textrm{PattyMaterialOf}( (s)_{0} ) \in \mathbb{Z}^{\omega^{\omega}}\)。
    4. 如果「「\((u0)\textrm{IsLessTechnicalThan}(t)\)不成立」和\( (\textrm{OddPattyOf}( t ))<s \)」, 則定義\((s)\textrm{IsBalancedFor}(t) := \perp\)。
    5. 如果「\(((u0)_{0})\textrm{IsBalancedFor}(t)\)不成立」, 則定義\((s)\textrm{IsBalancedFor}(t) := \perp\)。
    6. 如果\(\textrm{Lng}(u0) = 1\), 則定義\((s)\textrm{IsBalancedFor}(t) := \top\)。
    7. 定義\((s)\textrm{IsBalancedFor}(t) := ((u0)_{1})\textrm{IsBalancedFor}(t)\)。
  4. 如果「\((\textrm{IniSeg}(s,\textrm{Lng}(s) - 1))\textrm{IsBalancedFor}(t)\)不成立」, 則定義\((s)\textrm{IsBalancedFor}(t) := \perp\)。
  5. 定義\((s)\textrm{IsBalancedFor}(t) := (((s)_{\textrm{Lng}(s) - 1}))\textrm{IsBalancedFor}(t)\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{OddPattyOf} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \mathbb{Z}^{\omega^{\omega}} \\ s & \mapsto & \textrm{OddPattyOf}( s ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(\textrm{Lng}(s) = 0\), 則定義\(\textrm{OddPattyOf}( s ) := -1\)。
  2. 如果\(\textrm{Lng}(s) \leq 2\), 則定義\(\textrm{OddPattyOf}( s ) := EmptyPatty\)。
  3. 定義\(\textrm{OddPattyOf}( s ) := \textrm{IniSeg}(s,2) \frown \textrm{OddPattyOf}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 2) )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{PattyMaterialOf} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \mathbb{Z}^{\omega^{\omega}} \\ s & \mapsto & \textrm{PattyMaterialOf}( s ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(s\), 則\(\textrm{PattyMaterialOf}( s )\)未定義。
  2. 如果\(\textrm{Lng}(s) = 0\), 則定義\(\textrm{PattyMaterialOf}( s ) := -1\)。
  3. 如果\(\textrm{Lng}(s) \leq 2\), 則定義\(\textrm{PattyMaterialOf}( s ) := s\)。
  4. 定義\(\textrm{PattyMaterialOf}( s ) := \textrm{PattyMaterialOf}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 2) )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsLessTechnicalThan} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ ( s , t ) & \mapsto & (s)\textrm{IsLessTechnicalThan}(t) \end{eqnarray*} 用遞歸方法如下:

  1. 如果「「\((s)\textrm{IsPatty}\)不成立」或「\((t)\textrm{IsPatty}\)不成立」」, 則\((s)\textrm{IsLessTechnicalThan}(t)\)未定義。
  2. 如果\(\textrm{Lng}(s) = 0\), 則\((s)\textrm{IsLessTechnicalThan}(t)\)未定義。
  3. 如果\(\textrm{Lng}(t) = 0\), 則定義\((s)\textrm{IsLessTechnicalThan}(t) := \perp\)。
  4. 定義\((s)\textrm{IsLessTechnicalThan}(t) := \textrm{BaseOf}( s )<\textrm{BaseOf}( \textrm{PattyMaterialOf}( t ) ) \land (s)\textrm{IsIncludedIn}(\textrm{OddPattyOf}( t ))\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsEasyToEat} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ s & \mapsto & (s)\textrm{IsEasyToEat} \end{eqnarray*} 用遞歸方法如下:

  1. 如果「\((s)\textrm{IsHamburger}\)不成立」, 則\((s)\textrm{IsEasyToEat}\)未定義。
  2. 設想\(\textrm{Lng}(s) = 1\)成立。
    1. 如果\(\textrm{Lng}((s)_{0}) = 0\), 則定義\((s)\textrm{IsEasyToEat} := \top\)。
    2. 令\(u0 := \textrm{OddPattyOf}( (s)_{0} ) \in \mathbb{Z}^{\omega^{\omega}}\)。
    3. 令\(u1 := \textrm{PattyMaterialOf}( (s)_{0} ) \in \mathbb{Z}^{\omega^{\omega}}\)。
    4. 如果「\(((u0))\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    5. 如果「「\(\textrm{Lng}(u1) = 2\)和\(\textrm{Lng}(u0) \% 2 = 0\)」和\(\textrm{Lng}(u0) \geq 2\)」, 則如果「\( (u0)_{\textrm{Lng}(u0) - 2}<(u1)_{0} \)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    6. 如果「\(((u1)_{0})\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    7. 如果\(\textrm{Lng}(u1) = 1\), 則定義\((s)\textrm{IsEasyToEat} := ((u1)_{0})\textrm{IsBalancedFor}((s)_{0})\)。
    8. 如果「\(((u1)_{1})\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    9. 定義\((s)\textrm{IsEasyToEat} := ((u1)_{1})\textrm{IsBalancedFor}((s)_{0})\)。
  3. 設想\(\textrm{Lng}(s) = 2\)成立。
    1. 如果「\(((s)_{0})\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    2. 如果「\(((s)_{1})\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
    3. 定義\((s)\textrm{IsEasyToEat} := \neg( (s)_{0}<(s)_{1} )\)。
  4. 如果「\((\textrm{IniSeg}(s,\textrm{Lng}(s) - 1))\textrm{IsEasyToEat}\)不成立」, 則定義\((s)\textrm{IsEasyToEat} := \perp\)。
  5. 定義\((s)\textrm{IsEasyToEat} := (((s)_{\textrm{Lng}(s) - 2}) \frown ((s)_{\textrm{Lng}(s) - 1}))\textrm{IsEasyToEat}\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{NumberOfMeatIn} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \mathbb{N} \\ s & \mapsto & \textrm{NumberOfMeatIn}( s ) \end{eqnarray*} 用遞歸方法如下:

  1. 設想\((s)\textrm{IsHamburger}\)成立。
    1. 如果\(\textrm{Lng}(s) = 1\), 則定義\(\textrm{NumberOfMeatIn}( s ) := \textrm{NumberOfMeatIn}( (s)_{0} )\)。
    2. 定義\(\textrm{NumberOfMeatIn}( s ) := \textrm{NumberOfMeatIn}( (s)_{0} ) + \textrm{NumberOfMeatIn}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 1) )\)。
  2. 設想\((s)\textrm{IsPatty}\)成立。
    1. 如果\(\textrm{Lng}(s) = 0\), 則定義\(\textrm{NumberOfMeatIn}( s ) := 1\)。
    2. 定義\(\textrm{NumberOfMeatIn}( s ) := 1 + \textrm{NumberOfMeatIn}( (s)_{0} ) + \textrm{NumberOfMeatIn}( \textrm{FinSeg}(s,\textrm{Lng}(s) - 1) )\)。
  3. \(\textrm{NumberOfMeatIn}( s )\)未定義。

我定義一個可計算函數 \begin{eqnarray*} \textrm{Expand} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ ( s , n ) & \mapsto & s[n] \end{eqnarray*} 為\( s[n] := \textrm{Expand_Body}( s , \textrm{NumberOfMeatIn}( s ) + n , \Lambda( 0 ) , 1 )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{Expand_Body} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{N} \times \mathbb{Z}^{\omega^{\omega}} \times \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ ( s , n , t , m ) & \mapsto & \textrm{Expand_Body}( s , n , t , m ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果「「\((s)\textrm{IsHamburger}\)不成立」或「\((t)\textrm{IsHamburger}\)不成立」」, 則\(\textrm{Expand_Body}( s , n , t , m )\)未定義。
  2. 如果\(m > 3 ^ n\), 則定義\(\textrm{Expand_Body}( s , n , t , m ) := t\)。
  3. 令\(u0 := \textrm{ParseToHamburger}( m ) \in \mathbb{Z}^{\omega^{\omega}}\)。
  4. 如果\((u0)\textrm{IsHamburger}\), 則如果「「「\( t<u0 \)和\( u0<s \)」和\(\textrm{NumberOfMeatIn}( u0 ) \leq n\)」和\((u0)\textrm{IsEasyToEat}\)」, 則定義\(\textrm{Expand_Body}( s , n , t , m ) := \textrm{Expand_Body}( s , n , u0 , m + 1 )\)。
  5. 定義\(\textrm{Expand_Body}( s , n , t , m ) := \textrm{Expand_Body}( s , n , t , m + 1 )\)。

我定義一個可計算函數 \begin{eqnarray*} \Lambda \colon \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ n & \mapsto & \Lambda( n ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(n = 0\), 則定義\(\Lambda( n ) := (EmptyPatty)\)。
  2. 令\(u0 := (\Lambda( n - 1 )) \in \mathbb{Z}^{\omega^{\omega}}\)。
  3. 定義\(\Lambda( n ) := (u0 \frown u0)\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{ParseToHamburger} \colon \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ n & \mapsto & \textrm{ParseToHamburger}( n ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(n \% 3 \neq 2\), 則定義\(\textrm{ParseToHamburger}( n ) := -1\)。
  2. 定義\(\textrm{ParseToHamburger}( n ) := \textrm{ParseToHamburger_Body}( n / 3 , 0 )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{ParseToHamburger_Body} \colon \mathbb{N} \times \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ ( n , m ) & \mapsto & \textrm{ParseToHamburger_Body}( n , m ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(n < 3 ^ m\), 則定義\(\textrm{ParseToHamburger_Body}( n , m ) := (\textrm{ParseToPatty}( n ))\)。
  2. 設想\(n / 3 ^ m \% 3 = 1\)成立。
    1. 令\(u0 := \textrm{ParseToPatty}( n \% 3 ^ m ) \in \mathbb{Z}^{\omega^{\omega}}\)。
    2. 如果\((u0)\textrm{IsPatty}\), 則定義\(\textrm{ParseToHamburger_Body}( n , m ) := \textrm{ParseToHamburger_Body}( n / 3 ^ m + 1 , 0 ) \frown (u0)\)。
  3. 定義\(\textrm{ParseToHamburger_Body}( n , m ) := \textrm{ParseToHamburger_Body}( n , m + 1 )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{ParseToPatty} \colon \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ n & \mapsto & \textrm{ParseToPatty}( n ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(n \% 3 \neq 2\), 則定義\(\textrm{ParseToPatty}( n ) := -1\)。
  2. 定義\(\textrm{ParseToPatty}( n ) := \textrm{ParseToPatty_Body}( n / 3 , 0 )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{ParseToPatty_Body} \colon \mathbb{N} \times \mathbb{N} & \to & \mathbb{Z}^{\omega^{\omega}} \\ ( n , m ) & \mapsto & \textrm{ParseToPatty_Body}( n , m ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(n < 3 ^ m\), 則定義\(\textrm{ParseToPatty_Body}( n , m ) := (\textrm{ParseToHamburger}( n ))\)。
  2. 設想\(n / 3 ^ m \% 3 = 1\)成立。
    1. 令\(u0 := \textrm{ParseToHamburger}( n \% 3 ^ m + 1 ) \in \mathbb{Z}^{\omega^{\omega}}\)。
    2. 如果\((u0)\textrm{IsHamburger}\), 則定義\(\textrm{ParseToPatty_Body}( n , m ) := \textrm{ParseToPatty_Body}( n / 3 ^ m + 1 , 0 ) \frown (u0)\)。
  3. 定義\(\textrm{ParseToPatty_Body}( n , m ) := \textrm{ParseToPatty_Body}( n , m + 1 )\)。

\(EmptyPatty\)為\(\textrm{IniSeg}((-1),0)\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{BaseOf} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \mathbb{Z}^{\omega^{\omega}} \\ s & \mapsto & \textrm{BaseOf}( s ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果「\((s)\textrm{IsPatty}\)不成立」, 則\(\textrm{BaseOf}( s )\)未定義。
  2. 如果\(\textrm{Lng}(s) = 0\), 則\(\textrm{BaseOf}( s )\)未定義。
  3. 定義\(\textrm{BaseOf}( s ) := (s)_{\textrm{Lng}(s) - 1}\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{IsIncludedIn} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{Z}^{\omega^{\omega}} & \to & \{ \perp, \top \} \\ ( s , t ) & \mapsto & (s)\textrm{IsIncludedIn}(t) \end{eqnarray*} 用遞歸方法如下:

  1. 如果「「\((s)\textrm{IsPatty}\)不成立」或「\((t)\textrm{IsPatty}\)不成立」」, 則\((s)\textrm{IsIncludedIn}(t)\)未定義。
  2. 如果\(\textrm{Lng}(t) = 0\), 則定義\((s)\textrm{IsIncludedIn}(t) := \perp\)。
  3. 如果\(\textrm{Lng}(t) \leq 2\), 則定義\((s)\textrm{IsIncludedIn}(t) := s = t\)。
  4. 定義\((s)\textrm{IsIncludedIn}(t) := (s)\textrm{IsIncludedIn}(\textrm{FinSeg}(t,\textrm{Lng}(t) - 2))\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{Eat} \colon \mathbb{Z}^{\omega^{\omega}} & \to & \mathbb{N} \\ s & \mapsto & \textrm{Eat}( s ) \end{eqnarray*} 為\(\textrm{Eat}( s ) := \textrm{Eat_Body}( s , 0 )\)。

我定義一個可計算函數 \begin{eqnarray*} \textrm{Eat_Body} \colon \mathbb{Z}^{\omega^{\omega}} \times \mathbb{N} & \to & \mathbb{N} \\ ( s , n ) & \mapsto & \textrm{Eat_Body}( s , n ) \end{eqnarray*} 用遞歸方法如下:

  1. 如果\(s = \Lambda( 0 )\), 則定義\(\textrm{Eat_Body}( s , n ) := n + 1\)。
  2. 定義\(\textrm{Eat_Body}( s , n ) := \textrm{Eat_Body}( s[n + 1] , n + 1 )\)。
Advertisement