Subst' 規則A[y/y] ≡ A を使う。 y = C -----------[Subst'] A = A[C/y]代入法の原理Subt'とSymm, Tranを使う。 A = B y = C -----------------[Ass] A[C/y] = B[C/y]左変型規則と右変形規則 A = B --------[Left:A = A'] A' = B A = B --------[Right:B = B…

推論の構造規則回路図ではジャンクション。 無（恒等、NOP） 増（重複、コピー） 換（クロス） 放電器は入れない。また定数true（T、I）も入れないことにする。面倒になる割に恩恵が少ないから。推論の論理規則 略記号 役割 対応する射 Sel1 ∧-消去1 π1 Sel2…

僕には、既存のコースや教科書を踏襲する必然性も制約もない。だから、ようするに分かりやすくて短時間で説明が完了すればソレデイイノダ。手段は選ばん！となると、回路メタファーを使うのが早いだろうし、現実世界を記述する道具として位置づけた大きなラ…

演繹系（証明系）を、技術者の言葉で語ることが課題。まだ、いろいろと思案中だがね。まず、基本的な態度あるいは視点としては； 演繹系も計算システムであるので、通常のコンピュータシステムやプログラミング言語システム（言語処理系と実行環境）と同じだ…

高階関数をさまざまな側面から理解することが重要なのだ、と思う。 関数のパラメータ付けられた族（関数族） パラメータを、もう1つのの変数と思う たくさんの関数達の値をまとめて表示すると、2次元の表（マトリクス）になる これはすなわち2変数関数だろ …

あー 心残り もったいない せっかくだから もう少し あこもせも。

物理現象 f = <t|ut - (1/2)gt^2> とかの例を出してもよかったかな プロファイルの説明がゴッソリ抜けてた 僕は最近、X, Y→Z のような書き方をする（カンマを使う）、その理由も説明するといいかもな。 ×（かける）はX（エックス）と紛らわしい。 テンソル積は難しげな印象を与</t|ut>…

「言い忘れ」つうか、時間内に言い切ることに無理があった項目： 機械語と高級言語の境界線はない コンパイラとインタプリタの境界線はない テキストとバイナリの境界線はない 式と値の境界線はない（値としての式、値も一種の式） 世界は相対的、連続的 境…

絵を上下反転（鏡映）、左右反転させて描く 算術式のパースツリーをいろいろな方式で描いてみる 中間ノードに演算を描く方式と、末端ノードに演算を描く方式とか

中学校(?)の連立一次方程式。 定数、演算、文字（変数）で項、等号、等式として論理式を定義できる。 連立とは、∧で結ぶこと。 等式的理論（等式理論）の公理系と推論規則 例えば推移律は、 A = B B = C ---------------- A = Cと推論規則なのか、それとも推…

http://d.hatena.ne.jp/m-hiyama/20090221/1235192629 ： バイナリ関数コードφ∈NNが与えられると、f(x) = E(φ, x) としてfを再現できます。このことは、N→N という関数とNNのデータの間に1：1の対応があることを意味します。ただし、この1：1対応に関しては…

イータ変換までやるかな、それと、大きなラムダの基本概念とか - 檜山正幸のキマイラ飼育記 メモ編 時間が余ったらイータ変換とか、それは無理だ。やってみて分かったな。イータ変換ってば、関数の外延性（つうか、形式理論のなかの等号を外延的に解釈できる…

グラフとしての関数（外延）、計算ルールとしての関数（内包） 計算ルール＝式やプログラム、ifやcase分岐があってもよい ε記号や s.t. such that があってもいい、例：平方根 関数の等しさは超越的 現実的、実効的な等しさは何か？ f(x) = x(x+1), x^2 + x,…

関数の（超越的な）等しさが計算的に判断できたらオカシイはずだが、、、、嘘つきパラドックス＋対角線論法 のようなもんで、簡単だと思っていたが、アレレレ、出てこない。単に僕が頭悪いだけのようだ。[追記]全域性を判断できないことを経由すれば、関数の…

エミュレータ -- 例えば6809を586でエミュレートする。世にVMはいろいろあるしな。 スタンドアロンな（あるいは抽象的）コンパイラ -- 人間の行為を機械（のようなモノ）で代行する。 クロスコンパイラ -- 開発マシン上でコンパイラ・プログラムを動かす。 …

氏名公開のご承諾は当日その場で記入していただいて、アンケートのほうは後でメールというのがよさそうだな。

あの鉤括弧はUnicodeにあるのか？ '「'の鏡映文字があればいいんだな。とりあえずはG(-)とか書くテもあるが。本来、ゲーデル符号＝ゲーデル数は論理式とか証明とかに対して付けられている。構文領域から数領域への関数。だけど、構文領域に意味論があるなら…

ほんとに落語の話（咄）なのだが、頭山は再帰つうかスノーグローブ現象だよね。今朝の子供番組で「のっぺらぼう」も再帰構造だと知った。のっぺらぼうの娘さんに会ってビックリ、坂を駆け上って会った男の人がのっぺらぼう、という夢を見てさめて話した女房…

もともとは、2009年1月24日セミナー用だったが、「もしセミナーをやるなら」というネタはすべて「セミナー」タグに書くことにする。思い付きや小咄でも、それがセミナーの話題として使えそうなら「セミナー」タグを付ける。

僕が知る限り、自然演繹（他のシステムでもいいのだが）の証明過程を証明図のアニメーションだという説明を見たことがない。証明図が静的な図形のように語っている。これはいけない、これでは本質がわからない。計算も動的（時間的な推移）だし、証明も動的…

ひたすら計算とは違った感じで合成（結合）を扱ってみる。(f;g)(x) = g^・(f^・x) が成立することを示す。まず、を考える。正確には、<f, g, x| Exec(g^, Exec(f^, x))> だが略記した。これをフルカリー化すると <|λf.λg.λx.(g^・(f^・x) >、この引数なし関数（値はコンビネータ）をcとする。</f,>…

ラムダバブルを二重丸、三重丸で描くと少し図が簡略になる。そのとき、もとの（カリー化する前の）関数のアリティ（引数の個数）を知りたいなら、丸の数を0, 1, 2, ... と勘定し、それと、上に出ている線の本数を足す。丸の数は0から勘定する、なぜなら一番…

表記のような計算はまったく触れないことにした（http://d.hatena.ne.jp/m-hiyama/20090109/1231481303参照）。が、ネタは考えていたので後日の為列挙しておく。 λ(f, g).λx.g(fx) 合成 λx.λy.λz.x(yz) 同じく合成 チャーチの数と掛け算（足し算は難しすぎ）…

本編のhttp://d.hatena.ne.jp/m-hiyama/20070813/1186984585 「圏論的指数の周辺：ラムダ計算、デカルト閉圏、ノイマン型コンピュータ」とか、http://d.hatena.ne.jp/m-hiyama/20070816/1187250855「圏論的指数の定義」とかで述べているが、「fのラムダ抽象f…

土曜日の目標を、ベータ変換だけでなくイータ変換までにしようかと、もし可能ならだが。ガンマオペレーション＝脱抽象が、ラムダオベレーション＝抽象の逆であることを理解する。背景となる意味的な法則は： Exec(λt.(φ・t), a) = Exec(φ, a) である。ここで…

とりあえず、紙にメモすると散らばるから。 絵の描き方 上から下 f x と、左から右 抽象は右抽象 f^ タプリングは白丸 λも白丸（バブル） Applyは黒丸 タプルの抽象は、白丸と白丸を結ぶ ベキ（指数型）は二本線、逆向きの対 タプルのアリティ（項数）は、白…

自由変数 - 大域変数とは限らない。相対的な概念。PerlやJavaScriptでは？ 束縛変数（ラムダ変数） -- 位置引数であること、本質的に無名 大域環境、局所環境 -- ようするに環境、細かいこと言わなければ同じ。 PerlやJavaScriptでの実例を考える。あと、物…

言葉、立場、見方の多様性を強調 単眼と複眼、投影図と立体視 上江州流の紹介 絵算入門

立体視が重要 だが、複数の視点を紹介する時間がない 上江州流が中心 関数概念 「集合と関係グラフ」ベース、非常に静的 記号と計算（記号の書き換え）ベース 装置メタファー、直感的 矢印ベース、圏論へ 関数計算の基本演算 適用中心 結合（合成）中心 高階…

たいていのプログラミング言語のなかに埋め込める。 型：numberとboolean リテラル：普通 変数（インフォーマル）：a,b,c, x,y,zはnumber、p,q,r,s,tがboolean 名前付き関数と無名関数 算術演算子：+, -, *, %, 単項の- 組み込み関数： sqrt 論理演算子：&&,…