このブログの更新は X(旧Twitter)アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

参照用 記事

BNF の検索結果:

形式言語理論にも使える導出系

…方をします。例えば、BNF〈Backus–Naur form〉風に書けば:$`\quad \sigma_0 ::= i(\sigma_1, \cdots, \sigma_{n(i)})`$ 左右を反転させた書き方は:$`\quad (\sigma_1, \cdots, \sigma_{n(i)})i =:: \sigma_0`$ ノードを1つだけ持つツリー(開いたエッジがあるので正確には半ツリー〈semitree〉)で描けば:$`\quad \xymatrix{ {} \ar…

型理論の「代入」の分析

…arphi`$ は、BNF記法で次のように定義されます。$`\quad M ::= \xi \mid \theta \rev \varphi`$ $`\quad \varphi ::= () \mid \varphi \snoc (\xi := M)`$ここで、'$`\rev`$' は、オブジェクト構文レベルの引数渡し記号で、$`\xi`$ は変数名(を表すメタ変数)、$`\theta`$ はオペレーション名(を表すメタ変数)です。日本語散文で記述するなら: オペレーション項…

実用になる型理論の記法

…メタレベル構文であるBNF〈Backus–Naur form〉の記号とコンフリクトしてますが、別物です。「左辺は右辺で定義される」という意味では、BNF構文生成規則の '$`::=`$' と少し似てますが、オブジェクトレベルとメタレベルなので別物です。 [/追記]おわりにスターリングの構文にシンタックスシュガーをまぶしましたが、もとの構文・アイディアを本質的に変えたわけではなくて、単なる表層的な変更です。見た目が変わるだけのことなので、理論的なメリットはそのまま残されています…

GAT〈ガット〉の構文: スターリングの論文から

…ングのGAT指標の、BNF記法による構文生成規則は次のようです(原論文と僅かに変えています)。 指標 $`\mathbb{T} ::= \emptyset \mid \mathbb{T}, (\sigma : \mathscr{S}\mid \vartheta : \mathscr{O}) \mid \mathbb{T}, \mathscr{E}`$ ソート宣言本体 $`\mathscr{S} ::= [\Psi \vdash sort]`$ オペレーション宣言本体 $`\m…

球体集合達の圏の構文表示 2/2

…定義する方法として、BNF〈バッカス/ナウア形式 | Backus-Naur form〉(「コンピュータによる言語処理の常識」参照)のようなメタ記法もありますが、ここでは自然言語(の散文)もまじえて半形式的に定義していきます(次節から)。構文的データの定義正式な構文的データは、先頭にタグが付いたリストだとします。が、実際には略記を使います。タグが構文的役割りを表します。次の約束をします。 タグが $`\T{@foo-bar}`$ である構文的データ達の集合は $`{\bf F…

最近の型理論: 型理論の構文論と意味論

…「構文記述言語」は、BNF記法(「コンピュータによる言語処理の常識」参照)のように、構文を記述するための専用の言語です。上側中央は、構文と意味の関係を記述する言語で、スコットブラケットはこの言語に属する記号です。異なる言語に属する記号が、オーバーロードされたり同一視されたりします。それは、常に混乱のリスクを伴います。例えば、次は本来区别すべき記号の例です。 自然数の 5 を参照〈denote〉する通常使用言語の記号「5」と、対象言語の記号「5」 対象言語の変数名「x」と、対象…

フリーモナド 1: 自由で無料な木

…っても記述できます。BNF記法で生成規則を書いてみましょう(BNFに関しては「コンピュータによる言語処理の常識 // レキシング/パージングの実例」参照)。 Tree ::= @leaf X Tree ::= @node F(Tree)この生成規則は、帰納的な構成規則として読むことができます。 ベース: $`X`$ の要素にタグ $`\text{@leaf}`$ と付けたものはツリーである。 ステップ: 既に在るツリー(の集合)から$`F`$-コレクションを作り、そのコレクシ…

コンピュータによる言語処理の常識

…。文法規則の記述にはBNF〈バッカス/ナウア形式 | Backus-Naur form〉記法やその変種が使われることが多いです。BNF記法については: BNF記法入門(1)(2000年に書いた記事) この機会にマスターしようぜ、正規表現、構文図、オートマトン BNF、EBNF、ABNF、まー正規表現だな ここでの文法規則は次のようにしましょう。トークン型は角括弧で囲み、そうでない文法的な種別(非終端記号といいます)は丸括弧で囲むことにします。記号「::=」は、左辺が右辺のパタ…

Xy-pic/XyJaxについて調べてみた

…りません。構文記述のBNF〈Backus-Naur form〉がなんだか不正確な気がします。僕はちゃんと確認したわけじゃないですが、実際の挙動との食い違いや誤植(コマンド名綴り間違い)もあるようです -- 次のドキュメントで指摘されています。 "Commutative Diagrams with Xy-pic I. Kernel Functions and Arrows" by Paul A. Blaga "Commutative Diagrams with XY-pic I…

用語のバリエーション記述のための正規表現

…参照してください。 BNF記法入門(1)(19年前!の記事が残っていた) この機会にマスターしようぜ、正規表現、構文図、オートマトン BNF、EBNF、ABNF、まー正規表現だな 内容: 選択肢と省略可能 具体例 例 1 例 2 例 3 例 4 英語と日本語での例 ウンザリする例 選択肢と省略可能基本は次の二種類の書き方です。 選択肢: {A | B}AもBも同じ意味なので、どちらか一方を好きに選んでよいことを表します。選択肢がもっとたくさんあるときは、{A | B | C}…

論理式の集合とは何か?

…構文規則の記述には、BNF〈バッカス/ナウア形式〉が便利であり標準的でもあります。プログラミング言語に多少の馴染みがあるのなら、次の記事を読むと構文定義(や意味定義)の方法が手っ取り早く分かるでしょう。 プログラム意味論の書き方サンプル: UMiToL BNFに関しては、「UMiToL言語の構文」の節に簡単な例と他の記事への参照があります。というわけで、構文の定義にはBNFを使うことにします。構文定義の際に、項の定義と論理式の定義の二段階に分けます。項〈term〉とは、(今の…

プログラム意味論の書き方サンプル: UMiToL

…。念のために、構文をBNF〈バッカス/ナウア形式〉記法で定義しておきます。とても短い構文定義です。リテラルと変数については、後で詳しく述べます。EMPTYは、何もないことを示す目印です。 式 ::= リテラル | 変数 | '(' 式 ')' | 式 '+' 式 | 式 '-' 式 宣言文 ::= 'var' 変数 代入文 ::= 変数 ':=' 式 空文 ::= EMPTY 文 ::= 宣言文 | 代入文 | 空文 プログラム ::= 文 | プログラム ';' 文BNFや…

0引数関数と定数は同じなのか? :圏的ラムダ計算の立場から考える

…に、ラムダ式の構文をBNFで定義します。BNFの構文変数と対応する構文的要素の集合を同じ記号で表します。 Expr ::= Var | 'λ' Var ':' Type '.' Expr | Expr Expr | '(' Expr ')' ここで、'λ', ':', '.', '(', ')' はリテラルトークンです。この構文でのラムダ式の例は、λx:A.x (x∈Var, A∈Type)とか、(g f)λy:B.λx:A.y (f, g, x, y∈Var, A, B∈T…

キュリアの格上げによる総称の解釈

…ツリーリストの定義をBNF風に書けば、 List ::= ε | A List ここで、εは空リスト、Aはリストの項目となる構文要素です。「A List」は「AとListの単なる連接」ですが、プログラミング言語のデータ構造として考えるときは、consオペレータ(生成子、構成子)が必要です。Haskellのデータ定義風に書けば、 data List α = Nil | Cons α (List α) ここでNilは空リスト(あるいはリストの終端記号)を表します(これもデータ構成…

CSS3-JQuery時代のツリーパターン記述

…味を割り当てるには、BNF記法を使いましょう。例えば: simpleLi ::= <li>{text} BNFに関しては、「BNF、EBNF、ABNF、まー正規表現だな」、「お絵描きで学ぶ・無限正規ツリーとBNF(バッカス/ナウア形式)」などを参照してください。定数text典型的なツリー構造として、XMLのDOMツリーを考えましょう。そのノードには次の種類があります。 番号 記号定数 ノード種別 1 ELEMENT_NODE 要素 2 ATTRIBUTE_NODE 属性 3 …

要約版・明瞭正規表現

…。A Taxonomy of Finite Automata Construction Algorithms とかに詳しいようです(って、僕はこの論説読んでないけど)。 *2:A* は連接によるモノイド構造を持つとします。つまり、A* をAから作られた自由モノイドと解釈します。 *3:ツリー正規表現とツリーオートマトンに関する纏まった説明って、僕、してなかったんですね。断片的なら「お絵描きで学ぶ・無限正規ツリーとBNF(バッカス/ナウア形式)」とか「ツリーパターン入門」とか。

抽象構文記法に基づく構文記述と一般代数系

BNF(バッカス/ナウア記法)は、構文を正確に記述するためにとても便利です。僕はよく使ってますし、このダイアリーでもけっこう言及してますね。 https://m-hiyama.hatenablog.com/search?q=BNF BNFでは区切り記号や予約語なんかも具体的に記述しますが、パージングが終わった後のデータ(抽象構文木とか)では、区切り記号や予約語の文字や綴りはどうでもいいモノです。構文的なデータ構造だけが問題となります。パーズ済みデータをプログラムで扱うときは、…

ツリーパターン入門

…ぶ・無限正規ツリーとBNF(バッカス/ナウア形式) 参考2: この機会にマスターしようぜ、正規表現、構文図、オートマトン ツリーパターンの概要ツリーは有向グラフの一種で、ノードと辺からなります。ノードは小さい黒丸、辺は単なる実線(特に矢印は付けません)で描くことにします。ルートが上、リーフ(葉)は下に描きます。ノードや辺に対して名前や値を付けることはしません。したがって、同じ形状のツリーは同じとみなします。以下にツリーの例をいくつか挙げます*1。正規表現に'*'や'|'のよう…

意味記述のためのクロージャと記号表現

…とです(構文の記述はBNFで不満はありません)。CatyScript2.0で追加拡張する機能でたぶん最初に着手するのは変数とコマンド呼び出しです。よって、意味記述も変数とコマンド呼び出しを最初にやるでしょう。つうか、やってみました。やってみると、言語の表層構文以外に、評価の途中でだけ使うような構文的データ構造もあったほうがよいな、と思いました。「評価の途中でだけ使う」ヤツって、だいたいはクロージャなんですけどね。もっと具体的に言うと、コマンドのパラメータとか名前やら定義体(d…

データの部分構造とパート

…型 パートの利用例 BNFによるパート定義の構文 パートに関する制約と代数構造 その他のこと プロパティ/項目からパートへパートとは、“オブジェクトのプロパティ”や“配列の項目”を拡張した概念です。最初にプロパティと項目について復習しておきます。xが、JavaScriptやJSONのオブジェクトデータのとき、x.foo や x["foo"] でプロパティにアクセスできます。yが配列なら、y[2] のようにして項目にアクセスできます。代入は、x.foo = 10, x.[2] …

JSON向けのシンプルセレクター

…その他の拡張や略記 BNFによる構文定義 課題 構文の基本これから定義するセレクターは、ドットで区切ったフィールドアクセス式にワイルドカードを加えただけのモノです。基本的な特殊文字は次の4つです。 文字 説明 $ 与えられたデータ全体を表す . セレクターの各ステップを区切る区切り記号 * 任意のオブジェクト・プロパティを表すワイルドカード # 任意の配列項目を表すワイルドカード 基本セレクターは4種類です。 構文 説明 '.' 名前 名前により指定されるプロパティ値をセレク…

CatyScript2.0の変数概念

…を捨てるコマンド)。BNFによる構文記述はまた今度(>主にKuwataさん)。beginブロック変数のスコープは、だいたいはインタプリタが勝手に作ります。プログラマがスコープを制御したいならbeginグロックを使います。begin { /* ブロックの内容 */ } という形。beginブロックも式であり、ブロックの内容の値がbeginブロック(begin式)の値となります。beginの入り口で空な変数束縛環境が作られて、beginブロック内の代入式は新しい変数束縛環境に作用…

構文解析木とタグ付きJSON

… 算術式の構文は次のBNFで定義しておきます。 Expr ::= Term | Term '+' Term ('+' Term)* Term ::= Factor | Factor '*' Factor ('*' Factor)* Factor ::= Const | Var | '(' Expr ')'/* Constは整数リテラル、Varは変数名 */タグ付きJSONによる算術式の表現足し算を@SUM、掛け算を@MULT、括弧(parentheses)によるグルーピングを…

Wiki処理系を作る前に知るべきこと/考えるべきこと

…語の記述を補うためにBNFも併用します。 文字、文字列、テキスト、要素、内容、空白、区切り記号、データ文字、破棄文字、改行、行頭、行末、行、完全行、不完全行、空行、行頭空白、行末空白 文字以下で「文字」と言った場合、それはユニコード仕様で定義される印字可能文字と若干の特殊文字(後述)を意味します。Wikiマークアップされたテキストは、まず“文字の列”として認識されます。文字より低水準のレイヤー、バイトとかビットについては考えません。したがって、文字エンコーディングスキームには…

最近のCaty:型システムとクリーネ代数

…されます。集合Jは、BNF風の再帰的定義により次のように定義されます。 J ::= Scalar | Array Array ::= [J*] ここで、[J*] は、Jの要素を有限個(0個でもいい)を並べて外側をブラケットで囲ったデータを意味します。外側をブラケットで囲んで一纏まりにしていることがポイントです。シーケンス・データの領域単純化したJSONデータの領域Jだけでは不足です。Jの要素からなるシーケンスデータの全体をSとしましょう。コンピュータが実際に扱うのはJなんです…

この機会にマスターしようぜ、正規表現、構文図、オートマトン

…法 左線形文法 拡張BNF記法 正規表現 有限状態オートマトン 他に、クリーネ(クリーニ)代数や圏論を使った定式化もあります。フラクタル幾何や離散力学系にも正規言語やその拡張である文脈自由言語が出現します。詳細は形式言語の教科書を眺めてください。この記事では、暗黙にオートマトンのアルファベットと状態空間は有限だと仮定していますが、無限アルファベット/無限状態空間を考えることは重要です。現実のコンピュータのアルファベットや状態空間は有限ですが、あまりにも巨大な有限なので、無限で…

カジュアル過ぎるWikiCreoleを少しだけ厳密に

…です。軽量仕様では、BNFや型定義(スキーマ)を毛嫌いしているようですが、このテのフォーマルな道具なしに正確さを担保するのはほぼ不可能でしょう。比較的軽量なRFCだってABNFをヘビーに使っているしね。なんだかまるで振り子のよう。厳密だけど理解する気力を削ぐ仕様への反発から、容易に理解できる気分はするけど結局何を言ってるか分かんない仕様が色々と出てきています。どっちもマトモに実装できないか、あるいは勝手解釈な実装が色々出てしまうか。中庸は中途半端と似てるわけで、中途半端じゃな…

お絵描きで学ぶ・無限正規ツリーとBNF(バッカス/ナウア形式)

…・(B, C)これはBNF(バッカス/ナウア形式)の一種です。タプル (B, C) の前に付いている黒丸「・」は、図の「BとCを接合する黒丸」に対応していると思ってください。今話題にしている無限二分木では、AとBとCが同じ形状のツリーなので、そのBNFは次のように書けます。 A ::= ・(A, A)定義式の左辺にも左辺にもAが登場するので、これは再帰的な定義です。再帰的な定義は、「可能性としての無限」を導入します。また、再帰的な無限構造は循環的構造による表現が可能です。無限…

XMLからJSONへの変換はこうすべ -- eXtendedJSON-encoded XML

…ータは要素である。 BNFで書けば: 基本内容 ::= 文字列 | 要素 内容 ::= 基本内容 | list 属性付き内容 ::= {文字列値属性並び, "" : 内容} 要素 ::= タグ 内容 | タグ 属性付き内容 冗長性を避けるために表現をできるだけ短くしたいなら、次の処理をします。 リスト内で、連続する文字列は連結する。 リスト内で、空文字列は削除する。 @tag "" は @tag [] に置き換える。(短くはならないが、冗長性を排除) 長さ1のリストは、その項…

BNF、EBNF、ABNF、まー正規表現だな

BNFとか正規表現の話を。ミニマムなBNFと正規表現BNF(バッカス/ナウア記法)は、プログラミング言語の構文記述によく使われるメタ構文です。もともとは、「?」(省略可能)や「*」(任意回の繰り返し)のような記号は使わなかったようです。現在の正規表現で標準的に使われる「?」「*」「+」は、なくても次のように定義可能なのです。(以下で、EMPTYはそこに何もないことです。ほんとに何も無いと分かりにくいので目印にEMPTYを使います。) // X は A? X ::= EMPTY…