06. Math言語げんご

数式すうしきの表示対象ひょうじたいしょうを保たもち、その一部いちぶに対たいする厳密計算げんみつけいさんを独立どくりつした操作そうさとして公開こうかいする。parse/renderが数式すうしきを簡約かんやくしたり、等式とうしきの正ただしさを主張しゅちょうしたりしない。

全ぜんconstructorはmath-signatures参照さんしょう。Numberは有限十進ゆうげんじっしんの原表記げんひょうきを持もち、意味値いみちはBigRationalへ正確せいかくに変換へんかんする。整数せいすうp、分母ぶんぼqはq>0、gcd(|p|,q)=1、zero=0/1へ正規化せいきかする。Numberに格納かくのうできる値あたいは、約分後やくぶんごのqの素因数そいんすうが2と5だけの有理数ゆうりすうに限かぎる。これ以外いがいをNumberとして構築こうちく・decodeする場合ばあいはNonFiniteDecimalNumberで拒否きょひする。評価値ひょうかちのRationalはこの制限せいげんを持もたない。

任意有理数にんいゆうりすうから式しきを作つくるconstructor helper expression_from_rational は、有限十進ゆうげんじっしんならNumber、それ以外いがいなら整数せいすうNumberを子ことするFrac(Number(p), Number(q))を返かえす。元もとの構文こうぶんをlowerするときにこのhelperで著者ちょしゃのFracを折おり畳たたまない。frac 1 2 はFracのまま保持ほじする。Numberのprintはcanonicalな整数せいすうまたは有限十進ゆうげんじっしん（指数表記しすうひょうきなし、冗長じょうちょうな末尾まつびzeroなし、zeroは0）で、意味値いみちとsnapshotの一致いっちを確認かくにんした場合ばあいには元もとlexemeを表示ひょうじに利用りようできる。Number(1/3)をprint時じだけFracへ変換へんかんする設計せっけいにはしない。

Identifier leafは数学記号すうがくきごう。自由記号じゆうきごうfree symbolを許可きょかする。自由記号じゆうきごうはUnresolvedNameのエラーにしない。意味上いみじょうの入力要求にゅうりょくようきゅうとして列挙れっきょする。symbol "..." で予約語よやくごと同おなじ綴つづりや複数文字ふくすうもじの名前なまえを明示めいじできる。裸はだかのNameとsymbolの同おなじ綴つづりは同おなじ名前解決規則なまえかいけつきそくを使つかう。

letはinitを外側そとがわ、bodyを新あたらしい記号きごうscopeで読よむ。sum/integralのindexはbodyだけで有効ゆうこうであり、lower/upperでは外側そとがわを参照さんしょうする。自由記号じゆうきごうに架空かくうの定義位置ていぎいちを与あたえない。

subscript/superscript/scriptsは表示構造ひょうじこうぞう。一般いっぱんの添字そえじを配列はいれつアクセスや指数演算しすうえんざんに暗黙変換あんもくへんかんしない。代数的だいすうてきな累乗るいじょうにはpowを使つかう。callは数学すうがくの関数適用表現かんすうてきようひょうげんで、任意にんいのFnコード実行じっこうではない。

matrixは一ひとつ以上いじょうのrow、各かくrowは同おなじ正せいの列数れつすう。vectorは一ひとつ以上いじょうの要素ようそ。fenceは左右さゆうそれぞれ0または1Unicode scalar。空文字からもじで片側かたがわだけの括弧かっこを表あらわせる。

rootのdegreeが数値すうちliteralで0ならInvalidRootDegree。その他ほかの定義域ていぎいきはevaluate時じにも検査けんさする。表示ひょうじだけの式しきに実数じっすう/複素数ふくそすうの数値領域すうちりょういきを勝手かってに割わり当あてない。

CheckedExpressionが保証ほしょうするのは構造こうぞう・binding・既知きちの局所制約きょくしょせいやくであり、全記号ぜんきごうの値あたいや全演算ぜんえんざんの数値評価可能性すうちひょうかかのうせいではない。

BindingEnvironmentはMathAssignmentのassignments列れつであり、各かく要素ようそに名前なまえnameとMathExactValueのvalueを持もつ。名前なまえはUTF-8辞書順じしょじゅんで厳密げんみつに昇順しょうじゅんとし、重複ちょうふくと順序違反じゅんじょいはんを拒否きょひする。大文字おおもじと小文字こもじの同一視どういつしやUnicode正規化せいきかは行おこなわず、Symbolと同おなじTextを比較ひかくする。空からの環境かんきょうと未使用みしようの代入だいにゅうを許可きょかするが、未使用みしようでも値あたいの形状けいじょうを検査けんさする。検査済けんさずみ環境かんきょうは元もとの不変入力ふへんにゅうりょくを借用しゃくようし、名前なまえを二分探索にぶんたんさくする。名前なまえの未存在みそんざいは不正入力ふせいにゅうりょくや資源停止しげんていしと区別くべつし、自由記号じゆうきごうが未解決みかいけつの場合ばあいのSymbolic結果けっかに利用りようする。この検査けんさは式しきの全要求ぜんようきゅうの充足じゅうそくを証明しょうめいせず、NDF受信時じゅしんじにも順序じゅんじょと値あたいを再検査さいけんさする。

入力にゅうりょくはCheckedExpression、自由記号じゆうきごうのBindingEnvironment、Limits。出力しゅつりょくはExact(Value)またはSymbolic(expression, Requirements)。定義域違反ていぎいきいはん・形状不一致けいじょうふいっちは明確めいかくなEvalError。値あたいの種類しゅるいはScalar(Q)、Vector(List<Q>)、Matrix(rows,cols,List<Q>)、Truth(Bool)。

MathExactValueは評価値ひょうかちの言語中立げんごちゅうりつschemaであり、元もとのMathValueとは別べつである。ScalarとVectorとMatrixの要素ようそは任意にんいの正規形せいきけいRationalで、Numberの有限十進制約ゆうげんじっしんせいやくを適用てきようしない。Vectorは空からを認みとめず、Matrixのrowsとcolsは正せい、valuesは行優先順ぎょうゆうせんじゅんでrowsとcolsの積せきに等ひとしい要素数ようそすうを持もつ。次元じげんの積せきのU64 overflowも拒否きょひし、NDFの受信じゅしんでも同おなじ形状検査けいじょうけんさを行おこなう。この値あたいの検査けんさだけで元式もとしきの評価ひょうかや演算えんざんの定義域ていぎいきが証明しょうめいされたとは扱あつかわない。

評価ひょうかはsource順じゅんの左ひだりから右みぎ、純粋じゅんすい。letはinitを評価ひょうかしてからbodyを評価ひょうかする。未解決みかいけつの記号きごうに依存いぞんする部分ぶぶんはSymbolicとし、独立どくりつな数値すうちsubtreeの計算結果けいさんけっかを保持ほじできるが元もとの構文こうぶんを上書うわがきしない。

正確せいかくに評価ひょうかする演算えんざん:

integral、call、表示用ひょうじようtext/sequence/subscript/superscript/scriptsは、評価専用規則ひょうかせんようきそくがない限かぎりSymbolic(NotationOnly)。これらの表示ひょうじは完全かんぜんに対応たいおうする。解析的かいせきてきな積分せきぶんや任意関数評価にんいかんすうひょうかを実装済じっそうずみとしない。

MathML Coreの要素ようそをtyped Markupで生成せいせいする。Number=mn、Symbol=mi、表示ひょうじText=mtext、加減乗かげんじょう・比較ひかく=mrow+mo、frac=mfrac、sqrt=msqrt、root=mroot、sub/sup/scripts=msub/msup/msubsup、vector/matrix=mtable/mtr/mtd、総和そうわと積分せきぶん=munder/munderoverまたは対応たいおうするscript形けいをdisplay modeから決定けっていする。

暗黙あんもくのブラウザprecedence解釈かいしゃくへ依存いぞんしない。binding powerは比較ひかく10、add/sub20、mul30、neg40、pow50、atomic60。弱よわい子こを強つよい親おやへ入いれる際さいはmoによる可視括弧かしかっこを挿入そうにゅう。subの右側みぎがわ、powの左側等ひだりがわなど、同おなじprecedenceでも非結合ひけつごうな位置いちに括弧かっこを入いれる。fracは分子分母ぶんしぶんぼの構造自体こうぞうじたいがgroupになる。

数学表示すうがくひょうじの2項演算こうえんざんは元もとの順序じゅんじょを保持ほじする。mulのscalar/記号列きごうれつでも、読よみ違ちがいを避さけるためreference backendは中央点ちゅうおうてんを表示ひょうじする。callはfunctionと括弧付かっこつきarguments。sequenceは指定順していじゅんのmrowであり、勝手かってに演算えんざんを補おぎなわない。

letは「name := init ; body」のmrow。sumの下限かげんは「index = lower」、上限じょうげんはupper、bodyに必要ひつような括弧かっこを付つける。integralは積分記号せきぶんきごうと上下限じょうかげん、body、微分記号びぶんきごうdとindex。equalは表示ひょうじであって証明書しょうめいしょではない。

labelのDoc sentence annotationはsuiteがsafeなphrasing fragmentへ準備じゅんびし、mtextを介かいした注記ちゅうきとして出力しゅつりょくする。MathMLではlabelをmunderで表あらわし、最初さいしょの子要素こようそに数式すうしき、次つぎの子要素こようそにDocのXHTML phrasingを含ふくむmtextを置おく。複合演算ふくごうえんざんを注記ちゅうきする場合ばあいはbaseを括弧かっこで囲かこみ、注記ちゅうきの対象範囲たいしょうはんいと周囲しゅういの演算順序えんざんじゅんじょを保たもつ。hostは選択済せんたくずみのDoc rendererへ元もとのForeignClosureを渡わたし、同おなじBudgetで準備じゅんびと変換へんかんを行おこなう。Docの型かた・source・局所きょくしょlabelを検査けんさし、未解決みかいけつの外部要求がいぶようきゅうを保持ほじする。Math backendは返かえされたphrasingと結合後けつごうごの全表示経路ぜんひょうじけいろを検査けんさし、重複じゅうふくするHTML IDやblock内容ないようを拒否きょひする。MathMLの内容ないようモデルに適合てきごうしないblock内容ないようは受うけ入いれない。

interfaces/model.json のMath record/unionはconstructorの論理的ろんりてきな意味展開いみてんかいであり、Rust enum順じゅんや別べつの再帰さいきwire layoutではない。実値じつちのschemaは interfaces/math.json の MathSyntax / MathValue とする。MathRootはExpr / Row / DocGuestの3種類しゅるい。MathKindは29 formとNumber leafに対応たいおうし、bare SymbolNameは明示めいじSymbolと同おなじ意味いみkindへlowerする。子こはExprRef / RowRef / DocGuestRef、guestはEmbedRefで平坦へいたんなarenaを参照さんしょうする。schemaの明示めいじvariant名めいとfield列れつがwire tagであり、入力由来にゅうりょくゆらいの深ふかさをnativeの再帰所有さいきしょゆうへ転写てんしゃしない。

MathValueの構造検査こうぞうけんさはカテゴリ、参照さんしょう、到達性とうたつせい、cycle、共有きょうゆうDAGの最大経路さいだいけいろ、Number有限十進制約ゆうげんじっしんせいやく、vector/matrix形状けいじょう、fence幅はば、literal 0のroot degreeを検査けんさする。単独たんどくRowは空からを表あらわせるが、Matrixに取とり込こむrowの列数れつすうは正せいで全ぜんrow同一どういつでなければならない。この証明しょうめいはsymbol解決済かいけつずみCheckedExpressionや評価可能性ひょうかかのうせいの証明しょうめいではない。

MathSyntaxはsource宣言せんげん、元もとOrigin表ひょう、tokenごとのowner headを持もつMathView、SourceMapを所有しょゆうする。Number.spellingは Option<Span> のまま保持ほじし、存在そんざいする場合ばあいは宣言せんげんsourceとnode coverに整合せいごうする位置いちを指さす。意味いみRationalと原げんlexemeの一致いっちを証明しょうめいしたときだけ元表記もとひょうきをprintへ利用りようでき、位置構造検査いちこうぞうけんさだけをその証明しょうめいとみなさない。Symbol/Let/Sum/Integralの名前なまえoperandは閉とじたMathFieldLocationで選択位置せんたくいちとOriginを保持ほじする。本文ほんぶんの名前検索なまえけんさくで位置いちを再発見さいはっけんせず、source-lessの位置いちはNoneとする。

LabelのDoc annotationと独立どくりつDocGuestは、Doc SentenceのForeignClosureを保持ほじする。ownerの環境かんきょう・Origin ID・source/map閉包へいほうとguest自身じしんのID空間くうかんを混同こんどうせず、意味変換いみへんかんを行おこなわない。元構文もとこうぶんに意味的いみてきに不正ふせいなDoc annotationがあっても、Mathのsource構造検査こうぞうけんさを理由りゆうにDoc lowerや評価ひょうかを呼よび出だしてはならない。prepared表示ひょうじへ渡わたす意味いみ・内容ないようモデル検査けんさは別べつの要求ようきゅうとして残のこす。

lower::expression はhostが選択済せんたくずみparse/profileを確認かくにんしたSyntaxBundleと明示めいじMath表層ひょうそうSchemaRef/categoryを受うけ、現在げんざいのBudget/SourceAdmissionで再検査さいけんさしてMathSyntaxを返かえす。共有きょうゆうsourceは一度いちどだけ計上けいじょうし、原げんFrac・表示ひょうじscripts等などを簡約かんやくしない。局所きょくしょconstructor制約せいやくの失敗しっぱいは元もとのsource NodeRefとShapeErrorへ帰属きぞくさせ、破棄はきした出力しゅつりょくarenaのindexだけを位置情報いちじょうほうとして返かえさない。停止ていしは原げんStopReasonを保持ほじし、元構文木もとこうぶんきを変更へんこうしない。

初回しょかいNDF受信じゅしんはschema検査後けんさごに同おなじsource/Origin/View/guest閉包へいほうとarena制約せいやくを検査けんさする。宣言せんげんsourceの欠落けつらくをreceiverのambient storeから補おぎなわない。raw MathSyntaxの受信じゅしんはbinding・free symbol要求ようきゅう・評価結果ひょうかけっかのproofを発行はっこうしない。明示めいじconstructor helperは新あたらしいsource-less式しきを作つくるためのもので、元式もとしきを置換ちかんする処理しょりではない。

MathMLは独立どくりつした正式せいしきportable出力しゅつりょくであり、ブラウザがfont/layoutを担当たんとうする。Doc・MathのHTML生成せいせいは17章しょうのKaTeXPreferredを標準ひょうじゅんとし、生成環境せいせいかんきょうでKaTeXを実行じっこうしてCSS/fontと配布はいふする。忠実変換不能ちゅうじつへんかんふのう・生成能力不足時せいせいのうりょくぶそくじはNEPL3 MathMLへ診断付しんだんつきで切きり替かえる。閲覧時えつらんじにKaTeXを再実行さいじっこうせず、CLIがpixel描画びょうがまで行おこなうとも広告こうこくしない。

独自どくじlayout/rasterizerを追加ついかする場合ばあいは、CheckedExpressionまたはMathLayout入力にゅうりょくmodelを受うける別べつbackendとする。OpenType MATH tableやglyph outlineの実装都合じっそうつごうをMathの意味いみモデルへ持もち込こまない。

MathBindingsは構造検査後こうぞうけんさごのMathValueに対たいする束縛解析そくばくかいせきであり、CheckedExpression全体ぜんたいの証明しょうめいではない。MathBindingは束縛そくばくするformのoccurrenceとnodeを、MathSymbolUseは記号きごうのoccurrence・node・bindingを保持ほじする。bindingがNoneなら自由記号じゆうきごうであり、Someなら最もっとも近ちかい束縛そくばくformのoccurrenceを指さす。

occurrenceはrootを0として、意味いみfield順じゅんに子こをたどる先行順せんこうじゅんの番号ばんごうである。共有きょうゆうnodeも経路けいろごとに別べつのoccurrenceを持もち、RowとDocGuestにも番号ばんごうを割わり当あてる。DocGuestの内部ないぶは走査そうさせず、名前なまえは文字列もじれつの完全一致かんぜんいっちで比較ひかくする。

definitionsとusesはそれぞれoccurrence順じゅんである。sourceとOriginは入力にゅうりょくnodeのfield locationを参照さんしょうし、自由記号じゆうきごうに定義位置ていぎいちを作つくらない。NDF境界きょうかいでは入力にゅうりょくを指定していして再解析さいかいせきし、参照先さんしょうさき・出現順しゅつげんじゅん・過不足かふそくの不一致ふいっちをBindingMismatchとして拒否きょひする。全出現ぜんしゅつげんと名前比較なまえひかくに共通予算きょうつうよさんを適用てきようし、停止ていしした結果けっかを部分成功ぶぶんせいこうとして返かえさない。

free_symbolsはCheckedExpressionからMathFreeSymbolsを生成せいせいする。symbolsの各要素かくようそMathFreeSymbolはnameとoccurrencesを持もち、束縛そくばくされていない出現しゅつげんだけを同おなじ名前なまえにまとめる。nameはUTF-8の辞書順じしょじゅん、occurrencesは先行順せんこうじゅんとし、重複じゅうふく・欠落けつらくを認みとめない。

名前なまえは完全一致かんぜんいっちで比較ひかくし、大文字おおもじと小文字こもじの同一視どういつしやUnicode正規化せいきかは行おこなわない。定義位置ていぎいちや評価値ひょうかちを補おぎなわず、guestの内部ないぶも解析かいせきしない。NDFの受信じゅしんでは指定していされた入力にゅうりょくから再計算さいけいさんし、不一致ふいっちをFreeSymbolsMismatchとして拒否きょひする。共通予算きょうつうよさんの停止ていしは部分成功ぶぶんせいこうへ変かえない。

前置構文ぜんちこうぶんprinterは検査済けんさずみMath形状けいじょうを受うけ、Expr・Row・DocGuestのentryとsource textを返かえす。各出現かくしゅつげんをfield順じゅんに出力しゅつりょくし、Frac・pow・表示用ひょうじようscripts・labelを評価ひょうかや簡約かんやくで置おき換かえない。SymbolはsymbolとTextの明示形めいじけいを使つかい、束縛名そくばくめいがNameで表あらわせなければUnprintableNameとして拒否きょひする。共有きょうゆうnodeも出現しゅつげんごとに展開てんかいし、深ふかさ・出力しゅつりょく・作業量さぎょうりょう・確保量かくほりょうは呼出元よびだしもとの共通予算きょうつうよさんに従したがう。

DocGuestは正確せいかくな不変ふへんForeignClosureを同期どうきhost printerへ渡わたし、空からの応答おうとうやhostの失敗しっぱいを拒否きょひする。保持ほじsourceを無条件むじょうけんに代用だいようせず、Math coreはDocの評価ひょうか・I/O・provider選択せんたくを行おこなわない。hostが生成せいせいしたguest textと全体ぜんたいのsourceは、選択せんたくしたProfileで再さいparseして対応たいおうを検証けんしょうするまでroundtripの証明しょうめいではない。出力しゅつりょくには架空かくうのsource identityを付つけず、保存ほぞん・再さいparseを担当たんとうするhostが新あたらしいsnapshotを割わり当あてる。

MathEvaluationOutcomeは成功せいこうした評価ひょうかの交換値こうかんちであり、ExactにMathExactValue、SymbolicにMathEvaluationRequirementの列れつを持もつ。各要求かくようきゅうは元式もとしきのExprRefとMathEvaluationReasonを保持ほじし、評価順ひょうかじゅんに並ならぶ。sumの反復はんぷくで同おなじnodeの要求ようきゅうが生しょうじた場合ばあいも、出現しゅつげんごとの順序じゅんじょと重複ちょうふくを保たもつ。

受信側じゅしんがわはschemaとExactの形状けいじょうを検査けんさし、指定していされた不変ふへんの式しきと束縛環境そくばくかんきょうから再評価さいひょうかする。値あたい・要求ようきゅう・理由りゆう・順序じゅんじょが一致いっちしない結果けっかはEvaluationMismatchとして拒否きょひし、返却値へんきゃくちは受信値じゅしんちではなく再評価さいひょうかした結果けっかとする。受信じゅしんから照合しょうごうまで同おなじ予算よさんを使つかい、停止ていしを再試行さいしこうやSymbolicで消けさない。この交換値こうかんちは操作そうさの失敗しっぱいやproviderの通信契約つうしんけいやくを兼かねない。

MathEvaluationResultはSuccessにMathEvaluationOutcome、FailureにMathEvaluationFailureを持もつ。Failureは失敗しっぱいしたconstructorのExprRefと、OperandShapeMismatch・NotSquare・DivisionByZero・InvalidRootDegreeの種別しゅべつを持もつ。意味上いみじょうの失敗しっぱいも成功せいこうと同おなじく指定入力していにゅうりょくから再評価さいひょうかして照合しょうごうし、改変かいへんされた種別しゅべつや位置いちを拒否きょひする。cancel・資源停止しげんていし・内部不変条件違反ないぶふへんじょうけんいはんはFailureに変換へんかんせず、操作そうさのErrとして返かえす。providerの通信失敗つうしんしっぱいや要求ようきゅうidentityの照合しょうごうは、この数値評価すうちひょうかの結果型けっかがたとは別べつの境界契約きょうかいけいやくである。

printの具体的ぐたいてきな要求型ようきゅうがたはMathPrintRequest、結果型けっかがたはMathPrintResultである。要求ようきゅうは閉包へいほうを含ふくむMathSyntax、明示選択めいじせんたくしたDoc schema、MathPrintedGuest列れつを持もつ。guest応答おうとうは全体ぜんたいsyntaxのdigest、guest閉包へいほうのdigest、EmbedRef、textを含ふくむ。identity取得しゅとくとprint実行じっこうはcanonical値ちから別々べつべつにdigestを求もとめ、過去かこの検査けんさで予算よさんを支払済しはらいずみとはしない。未選択みせんたく、選択せんたくしたschemaとの不一致ふいっち、欠落けつらく・重複じゅうふく・空からのguest、digest不一致ふいっちをInvalidで拒否きょひする。Sentence以外いがいのguest categoryは、identity計算前けいさんまえの構造検査こうぞうけんさで入力境界にゅうりょくきょうかいのErrとして拒否きょひし、Invalid結果けっかへ変換へんかんしない。Completeだけが完全かんぜんなartifactを返かえし、停止ていしは元もとのStopReasonを保持ほじしたStoppedとなる。構造不正こうぞうふせいは入力境界にゅうりょくきょうかいのErrであり、受信じゅしんした結果けっかdataだけから実行じっこうproofや遠隔えんかくUsageを信用しんようしない。生成せいせいと停止後ていしごのtransport encodeは別べつの処理しょりであり、print途中とちゅうのBudgetを交換こうかんして成功せいこうさせない。

MathSourceArtifactはtextとMathCategoryを持もち、Expr・Row・DocGuestの再さいparse入口いりぐちを区別くべつする。portableのencode/decodeはschema適合てきごうdataを扱あつかうだけで、生成元せいせいもとの証明しょうめいではない。verifyは要求ようきゅうの不変ふへんMathと選択せんたくhostから同おなじBudgetでprefixを再生成さいせいせいし、textとcategoryの完全一致かんぜんいっちを検査けんさする。不一致ふいっちをMismatchとして拒否きょひし、成功時せいこうじも返かえすのは局所生成きょくしょせいせいしたartifactである。guestの意味同等性いみどうとうせい、provider要求ようきゅうidentity、保存先ほぞんさきsnapshot、失敗応答しっぱいおうとうのtransportは別べつの契約けいやくとして検査けんさする。

lower、check、free_symbols、evaluate、print、render_mathml。評価結果ひょうかけっか、部分評価ぶぶんひょうかの新式しんしき、元もとの式しきを別値べつちとして返かえす。文書側ぶんしょがわのrender要求ようきゅうがevaluateを自動じどうで要求ようきゅうしない。