『 1. プログラムの理論とは何か』

プログラム理論とは，プログラムの性質について数学的に正確に述べるのに必要な枠組を作るためのあらゆる理論の総称である．...中略... 本章では，...中略... 技術的な詳細ではなく，それの底にある考え方，すなわち，記号と意味の関係，記号論理，記号の表現形式といった点に重点をおいて説明する．

Nobuo Yamashita

『1.1 記号と意味』

何か物事について正確に述べようとするとき，まず必要になるのは正確な表記法である．表記とは物（対象）に名前を付けることであり、名前というのは適当な記号の列である．... 中略 ... こういう状況を，記号列が対象を指示しているとか，記号列が対象を表現していると言う．... 中略 ... 今必要なのは数学的に正確な表記法であり，それは記号を組織的に組み合わせて必要な一連の記号列を得る方法である．この段階では各記号列がどういう対象を指示しているかを考えずに生成できなければならない．

Nobuo Yamashita

nat記号列

ここでこれから使う例のため，□ と ◇ という2つの記号を導入して，その2つの記号からなる記号列で，nat記号列というものを次のように定める．

□ は nat 記号列である．

α が nat 記号列ならば，α・◇ は nat 記号列である．ただし・は2つの記号列をつなげる操作を表している．

Nobuo Yamashita

対象記号（object symbol）
メタ記号（meta symbol）
メタ変数（meta variable）
メタ言語（meta language）

Nobuo Yamashita

nat記号列がいま扱いたい対象を指示している記号列全体であるとしよう．nat記号列が指示する対象上の演算を表現したいとすると，それはnat記号列に対する適当な記号操作として定めるのであるが、これも記号列がどういう対象を指しているかとは関係なく純粋に記号の操作として定めなければならない．

Nobuo Yamashita

newtype Symbol_ a = Symbol_ a
type NatSymbol = Symbol_ Char
_Square :: NatSymbol
_Square = Symbol_ '□'
_Diamond :: NatSymbol
_Diamond = Symbol_ '◇'
fromNatSymbol :: NatSymbol -> Char
fromNatSymbol (NatSymbol_ c) = c
toNatSymbol :: Char -> NatSymbol
toNatSymbol = \ case
    '□' -> Symbol_ '□'
    '◇' -> Symbol_ '◇'
    c    -> error ("Not a Nat Symbol: " ++ show c)

newtype SymbolString_ a = SymbolString [a]
type NatSymbolString = SymbolString_ NatSymbol

(・) :: SymbolString_ a -> SymbolString_ a -> SymbolString_ a
SymbolString_ ss ・ SymbolString_ ts = SymbolString_ (ss ++ ts)

singleton :: Symbol_ a -> SymbolString_ a
singleton x = SymbolString [x]

_Nat1 :: NatSymbolString
_Nat1 = SymbolString_ [_Square]
_Nat2 :: NatSymbolString -> NatSymbolString
_Nat2 α = α ・ singleton _Diamond

Nobuo Yamashita

P 記号列

現在の例に新たに $P$ という対象記号を追加して， $\alpha$ と $\beta$ が nat 記号列のとき $\alpha P \beta$ という記号列を P 記号列と呼ぶことにする．P 記号列を変形して nat 記号列を得る手順を以下のように定める．

$□P\beta$ は $\beta$ に変形される

$\alpha◇P\beta$ を変形するには，まず $\alpha P \beta$ を変形しその結果を得る．それを $\gamma$ とすると $\alpha◇P\beta$ は $\gamma◇$ に変形される

Nobuo Yamashita

_P :: Symbol
_P = Symbol_ 'P'
type PSymbolString = SymbolString_ Symbol

_PSymbolString :: NatSymbolString -> NatSymbolString -> PSymbolString
_PSymbolString α β = α ・ singleton _P ・ β

transform :: PSymbolString -> NatSymbolString
transform = \ case
    SymbolString_ ss -> case map fromSymbol ss of
        '□':'P':β -> SymbolString_ (map toSymbol β)
        cs        -> case break ('P' ==) cs of
           (α,_:β)    -> case map toSymbol (init α) of
               γ          -> γ ・ singleton _Diamond