2022-07-01から1ヶ月間の記事一覧
$`\newcommand{\deduce}{ \mathop{\|\!-} }% \newcommand{\afford}{ \mathrel{\|} }% \newcommand{\Sign}[1]{ \mathscr{#1} } %`$$`\Sign{A}`$ は背景指標〈background signature〉として、シーケント $`\Gamma \to A`$ が演繹可能〈deducible〉であることを…
とりあえず、Leandで使っているキーワード。証明には限らないモノ。 コメント -- （ハイフン2個、行末まで） コメント /- -/ ==> ラムダ記法の一部、ピリオド相当 fun 〈λ〉 def := let := ; （ローカル定義、in ではなくて ;） variable （変数の予約） sec…
まず重大な注意： npm i svg.js と npm i @svgdotjs/svg.js では違うものがインストールされる。 Plumb > npm list +-- @svgdotjs/svg.js@3.1.2 +-- @types/jest@28.1.4 +-- @types/node@18.0.3 `-- svg.js@2.7.1 svg.js は開発が止まっているかも知れない。…
NPMによるスキャフォールド - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。npx ≡ npm exec の一時インストール先だが、Linux で ~/.npm/_npx/ らしいがWindowsでは %USERPROFILE%/AppData/Local/npm-cache/_npx/ ここを見ると確かにパッケージがインスト…
最近は、NPMだけでプロジェクトのスキャフォールディングができるようだ。例えば、vite〈ヴィート〉のセットアップは： npm create vite@latestnpm create は npm init の別名〈エイリアス〉、i.e. npm create <initializer> ≡ npm init <initializer> 。npm init のマニュアルは： htt</initializer></initializer>…
<html> <head> <meta charset="UTF-8" /> <title>Import JSON</title> </head> <body> <script type="module"> import myJson from './external.json' assert {type: 'json'}; console.dir(myJson); </script> </body> </html> いくつか問題がある。 import/assert はまだ対応してないかも知れない。assertなしでも、拡張子で判断してJSONファイルをインポー…
大小関係、最小限と足し算との協調性 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 を再掲。 証明要求： Γ |-? ∃a.∀x.a≦x BEGIN ∀-BOX var u 0 + u = u --[●∃導入 t:←左辺のu] ∃t.0 + t = u 0 ≦ u --[●∀導入 x:←u] ∀x.(0 ≦ x) END ∀x.(0 ≦ x) --[●∃導入 a:←0…
導出： false-elim ＝ initial : ⊥ → P true-intro ＝ final : P → T forall-elim ＝ instantiate ＝ projection : ∀x∈X.P(x) → P(a) exists-intro ＝ uninstantiate = injection ： P(a) → ∃x∈X.P(x) リーズニング： Forall-Intro-Right :: (x∈X. φ(x):A→P(…
全ての道はRomeへ続くのか - これからのJavascript開発を考える に、Rome の情報あり。そこにあったツールの分類： トランスパイラ（Babel,esbuild,SWC） バンドラ（webapck,Parcel,rollup） 型チェック（Typescript,flow） リンター（ESLint） フォーマッタ…
DOMツリーが完了しないと、DOM操作はうまくいかないが、この程度だとbodyの最後にscriptを書けば問題ないようだ。 <html> <head><title>SVG Test</title></head> <body> <h1>Hello SVG</h1> <script> const svgNS = "http://www.w3.org/2000/svg"; var body = (document.getElementsByTagName("body"))[0]; var svg = </body></html>…
ツールの分類が難しい。境界線がハッキリしないし、実際複数の役割を兼務しているソフトウェアが多そうだ。つまり、だいぶ機能重複があるってこと。 バンドラー： 複数のファイルをまとめて単一または少数のファイルにする。 互換性トランスパイラ： JavaScr…
使う言葉： 述語 → (述語関数 | 述語記号) 命題〈単純命題〉 構造化命題〈structured proposition〉 導出〈derivation | デリベーション〉 シーケント リーズニング 背景指標 導出可能〈derivable | デライバブル〉 使わない言葉： 判断 証明 推論 推論規則 …
排中律 Law of excluded middle を、Principle of Bivalence ともいうのか。「二値性の原理」かな。 矛盾律 Law of contradiction （無矛盾律 Law of noncontradiction）は、排中律の双対になっている。 T ----------- 排中律 (A | ￢A) (A , ￢A) ---------…
比較的に概念的な話、雑多： HTML element と DOM node は同義語だと思ってよい。 connect elements とは、DOMノードを繋ぐ行為。 コネクションという名詞は、繋がれた要素／ノード達からなる構造物を指す名詞。 コネクションを作る行為を表す動詞が connect…
名前〈記号〉とモノを区別できない。a と [[a]] （スコットブラケット）で区別する。 命題と主張を区別できない。P と |- P で区別する。 要素と集合を区別できない。a ∈ A で区別する。 内包と外延を区別できない。A = {x∈A | P(x)} で区別する。 所属と…
概念編： コネクションがjsPlumbの中心概念。コネクションは次の相互依存した5つの概念にブレークダウンされる。 アンカー エンドポイント コネクター オーバーレイ グループ 言葉の響きと違う意味もあるので注意（いつものことだが）。 Graphvizとの対比で…
コミュニティバージョンと有償バージョンあり。コミュニティバージョンのドキュメントは https://docs.jsplumbtoolkit.com/community 。サンプルの一枚HTMLは： https://gist.github.com/productivity-for-programmers/6ef09ef5ccd5ab62a2d259d4c7260376 パ…
とりあえず、とりあえず： JSX構文は、HTMLに近いが違うマークアップ言語だと思えば（割り切れば）いい。 テンプレート変数〈プレースホルダー〉は { } 構文。テンプレート構文としては視認性が落ちるが、まーしゃーない。MDXでもエスケープはブレイスだけ。…
次元0 ワイヤー、ケーブル ⊥： 波線 T： 破線 A: 実線 Γ： 実線または幅付き線 次元1 ノード次元1 AND X_{Γ, Σ} ： スワップ Γ # Σ → Σ # Γ Δ_Γ ： 分岐 Γ → Γ # Γ !_Γ ： 削除 Γ → T π^1_{A, B} : 横線 (A, B) → (A) π^2_{A, B} : 横線 (A, B) → (B) ∧_{A, …
指標はラベル〈名前〉の宣言文だけを並べたもの。別名は： セオリー： 指標をセオリーと呼ぶ人がいる。 文脈〈コンテキスト〉： 型理論ではよく使う。特に型シーケントの仮定側を文脈と呼ぶ。 束縛： 型付きラムダリストに現れる宣言の並びは束縛と呼ばれる…
TypeScriptで宣言空間という独特の言葉を使う。「名前空間」と呼ばない理由は： 「名前空間」はファイルとは別なモジュールを意味するので、コンフリクトを避けた。 名前の容れ物というより、名前の分類基準に近い。 宣言された名前がどの種別かは： 変数名…
パッケージマネージャーとビルドツールは必要。 パッケージ直下の階層の存在物はモジュールでいいと思う。モジュールは物理ファイルに対応がわかりやすい。 スケルトンが何であるか？ の位置付けがよく分からない。 ビルドツールとバンドラーの境界線は確か…
宣言・定義ペアの完全な記述は under D assuming Σ declare k-x-mor f :k Γ →k A in M define f := Eここで： D はドクトリン。ドクトリンはメタ指標と文法からなる。ドクトリン配下の指標は、ドクトリンが定義した文法により記述する。 シグマは背景指標。…
\$WinREAgent\ 無害な一時ファイルらしい → https://amksystem.com/tech/win10-hidden-folder-winreagent/ \trdock_debug.log → https://forums.lenovo.com/t5/Pre-Installed-Lenovo-Software-and-Applications/C-trdock-debug-log-is-constantly-appearing-…
セクションという呼び名が適切かどうか分からない（暫定）だが、そう呼ぶとして、セクションの構成素は： 背景指標 Γ 新規導入指標 Σ 定義済み指標 Δ 構成手続き φ : Γ+Σ → Δ セクションから、次の構成手続きも出来る。 φ': Γ+Σ → Γ+Δ Σは、次の可能性がある…
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages Sebastian Ullrich, Leonardo de Moura https://arxiv.org/abs/2001.10490 またはPDF https://lmcs.episciences.org/9362/pdf
choco upgrade chocolatey コマンでアップグレードしたが失敗。なんかグチャグチャになってしまった。OneDriveの“ドキュメント\”パスが関係しているようだが、よくワカラン。最初からインストールし直しするしかなさそうだが、choco使うのやめようかな。WinG…
過去の記事をまとめてメモとする。ザッと読んで思い出すには便利だと思う。 シェブロテインのレコーディングフェーズとGAST - (新) 檜山正幸のキマイラ飼育記 メモ編 GAST〈ガスト〉はグラマーASTのこと パーザークラスのコンストラクタが呼ばれると自己分析…
section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int＼{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, …
Leanにも、NPMパッケージと同様な仕掛けがあるらしい。 ディレクトリがパッケージ メタデータが leanpkg.toml 一部のメタデータは leanpkg.path にある。 ツールの情報がメタデータに書いてあって、パッケージをダウンロードした先で環境を再現できるように…
