📏Refal言語入門 Graphs 縮約(contraction) 代入(assignment) 制約(Restriction)
代数的には、パターンマッチンググラフは、パターンマッチングの操作の3種の積の和であり、積は逐次実行を、和は並列実行を意味する
縮約(contraction)とは、v ：p のパターンマッチングで、vは変数、pはリジッドパターンであり、この縮約をv-(c)->pとする。代入(assignment)とは、eを式、vを変数とするe:vにマッチするパターンである。この代入を e <-a- v と表記する。制約(Restriction)とは(# G)のことで、Gは縮約グラフ、すなわち縮約のみからなるパターンマッチングのグラフである。これは、G中の少なくとも一つの縮約パスが成功すればZ(impossible operation, failure)と評価され、そうでなければID操作I(do nothing)と評価される。
この表記は（特に代入の表記は）珍しいと思われるかもしれないが、論理的であり、非常に便利である。これは次の2つの原則から導かれる。(1) 左側には束縛された（古い、定義された）変数があり、右側には自由な（新しい、これから定義される）変数がある。(2) 操作が置換と理解される場合、矢印は変数からその置換に向けられる。
私は、パターンマッチングの演算の代数について、同値性の関係 のセットを開発し、SCP-3 のプログラミングはそれに基づいて行わ れたが、残念ながらこの理論はまだ発表されていない。理論の初期段階 は [40] で見ることができる。最も重要な同値関係は、同じ変数に対する代入と縮約の衝突であ り、これはマッチングで解決される。
Refalグラフでは、運転はパターンマッチング操作のための整流関係の応用である。関数定義に現れ、Refalマシンの1ステップを表す正規形の歩みは、CRAという構造をしており、文字はそれぞれContraction、Restriction、Assignmentを表している。2つのステップを表すウォークはC1R1A1C2R2A2である。衝突A1C2を解決し、縮約と制限を整流関係に従って調整すると、歩みは正規形CRAに戻る：1ステップの駆動を行ったことになる。
お願い致します