サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
Pixel 9
ie.u-ryukyu.ac.jp/~kono
Agda Programming †1 Agda1) Haskell2) Dependent type Agda Agda Agda Emacs Agda Dependent type Agda Agda Agda Agda Curry Howard 3) Dependent type ( ) Agda ? Agda Agda Programming Technique in Agda Shinji KONO †1 1. 80 ML HOL4) Agda1) Curry Howard Haskell2) Agda Haskell I/O Monad 5) Monad (Cate- gory theory)6) †1 Information Engineering, University of the Ryukyus. Monad (Adjoint pair) Kleisli Monad M
Menu Menu top : Agda による圏論入門 可換図 HomReasoning.agda 自然変換を理解すれば圏論は終わったようなものですが、さらっと可換とか書いてある割に良くわからないものです。そもそも自然変換とはなんなんのか? Agda を使うと理解できるようになるんでしょうか? 自然変換は二つの Functor : A -> B に対して定義されます。ということは、二つの圏A,B が関係しています。以下の図が可換になると簡単に説明されているのが普通です。 F(f) F(a) ---→ F(b) | | |t(a) |t(b) G(f)t(a) = t(b)F(f) | | v v G(a) ---→ G(b) G(f) これは、可換あるいは可換図の定義だと思うべきです。図は人用のもので、Agda にとっては、 等式 G(f)t(a) = t(b)F(f) だけが重要です。
A x N (N は計算量) Monad の例題 部分計算 計算には例外が付きものである。例外として未定値を返せる計算を考えよう。この時に、返す値は、通常返される値と、未定値のSum型になる。型変数を持つデータ構造は Functor だったのを思い出して、 data maybe {c : Level} (A : Set c) : Set c where just : A → maybe A nothing : maybe A Maybe : Functor Sets Sets Maybe = record { FObj = λ a → maybe a ; FMap = λ {a} {b} f → fmap f ; isFunctor = record { identity = extensionality {zero} ( λ x → ? ) ; distr = extensionalit
Menu プロセスとカーネル プロセスは、一つのコンピュータに、仕事のまとまりを作る。これは、あたかも、そのプロセスが一台のコンピュータを一人で使っているように見える。プロセスには以下の要素が付属している。 メモリ CPU時間 コンテキスト 複数のプロセスが互いに、不法な方法で干渉しないように、ハードウェアとオペレーティングシステムが管理を行っている。 プロセスの作り方 ここでは、zsh からのプロセスの作り方を勉強しよう。 コマンドの起動 停止 並列実行 バックグラウンドで実行 script の取り方 zsh の設定 コンピュータとバス ie.u-ryukyu.ac.jp system configuration CPU と外部の機器をつなぐ、バスとチップがある。 CPU から見れば、それはメモリにしか見えない。(I/O port を特別扱いするCPUもある) CPU レジスタの集まりと
Menu Menu top : Agda による圏論入門 ここで使われている例題は、 Category exercise in Agda に置いてあります。 Agda の install の方法 Homebrew を使うのが良いそうです。 Emacs を先に入れます。 brew tap caskroom/cask brew cask install emacs その後、 brew install agda GHCが入ってないなら、 brew install ghc install 先がどこかは、 /usr/local/Cellar/agda/2.5.2/lib/agda などになるので、~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。 init.el GUI 側で使わないと文字化けすることがあるようです。 Terminal
Menu Menu Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。 Higher-Order Categorical Logic の 0章に相等する内容です。 BitBucket category-exercise-in-agda source code Agda の入門の要約 Agda の入門 Agda の集合の Level Agda の record Agda のReasoning Caategory module と圏の入門 自然変換 IdentityFunctor と Hom Reasoning Monad の結合則 Sets と Monoid を使った Monad の例 Kleisli 圏の構成 ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。 Adjoint から Monad を導く Kleisli 圏による Mona
目次 10. ブロックと手続きオブジェクト これは、Rubyに数あるクールな特色のなかでもその際たるものです。 ほかの言語の中にもこの特徴を持っているものがありますが、そこでは (クロージャー などの)他の名前がついています。 でも、ほとんどの有名なプログラミング言語にはないものです。 では、このクールな新しいこととはいったい何でしょう。 それは、コードのブロック を作って(doとendの 間のコードをこういいます。)、それをオブジェクトとしてくるんで (手続きオブジェクト(proc) と呼びます。)、変数に保存したり メソッドに渡したりして、それでもって、そのブロックの中のコードは好きな時に (何度でも)実行させることが出来るという能力です。 なので、この特徴はメソッドと似ているのですが、これがオブジェクトに付属しているものでは ないところが異なります(それ自身 がオブジェクトなのです
Menu Menu OSを落とすのは死亡フラグ 3年次4年次は忙しい OSの授業は3年次4年次で使うためのもの 情報工学科は パソコンの使い方を教えてくれるところではありません ソフトやハードの作り方を学ぶところ チェックリスト 情報工学科の卒業生は専門家 専門家は何を知っているべきか? 自分で動かしてみない限り身につかない 自分がどれくらいの時間でできるのか 他人がどれくらいの時間でできるのか この問題はどれくらいの時間がかかりそうか 量が多い 2週間ではできません でも、40題程度。1日1題で2ヶ月かからない とにかくやれ 人に聞けない技術者は終わり ぐぐってもムダ 英語で探せ コピーする時には、コピー先を明記する それ本当に正解? 英語の使えない技術者は必要ありません 英語が使えるか使えないかで職種がわかれる 英語を嫌い、使えなくなるように教育されている iTP 100を目標にする(
Menu Menu この授業では、Haskell と Agda を使って、ソフトウェアの信頼性を高める手法の一つである証明について学びます。 参考書 「やさしい Haskell 入門 (バージョン98)」 すごい Haskell Miran Lipova 達人プログラマー アンドリュー ハント、デビッド トーマス (ピアソン・エデュケーション) オブジェクト指向における再利用のためのデザインパターンエリッ ク ガンマ (著), ラルフ ジョンソン (著), リチャード ヘルム ( 著), ジョン ブリシディース (著), Erich Gamma (原著), Ralph Johnson (原著), Richard Helm (原著), John Vlissides (原著), 本位田 真一 (翻訳), 吉田 和樹 (翻訳) プログラミング作法 ブライアン カーニハン (著), ロブ パイク
Menu Menu まず、プロジェクトを Xcode4 で作ります。 File->New Project から、Command Line Tool そこで、Next としていきますが、 名前は、FileCopy (例です) Source local git repository for this project にチェックをいれます。 Project folder で git をチェック cd FileCopy して、git log | cat すると、すでに Initial Commit されます。 Remote repository をサーバ上に作る ここからは、サーバ上で操作します。 % ssh yomitan.ie.u-ryukyu.ac.jp % cd /net/home/git/teacher/kono % mkdir -p os/FileCopy % cd os/FileCo
目次 7. 配列とイテレータ 好きな数だけ単語の入力をしてもらい(1行に1単語、最後はEnterだけの空行)、 アルファベット順に並べ変えて出力するようなプログラムを書いてみましょう?いいですか? さて、最初に・・—えーと、あー、ふむふむ。 何を使えばいいのかというと— あーと、んーと。 まだ出来ないようです。まずは、いくつあるかわからない数の単語を保存する方法と、 その全部をどうやってまとめるのかを知らないとだめですね。 これが分かれば他の変数とはごっちゃにならないですみます。 何か一覧表(list)のようなものに単語を入れないといけないようです。 つまり配列 が必要です。 配列とはコンピュータの中の一覧リストようなものです。 リストの中のすべての項目は変数のように振舞います。 特定の項目が何のオブジェクトを指し示しているかを知ることが出来るし、 それを別のオブジェクトにポイントしなお
目次 0. はじめに プログラミングをするためには、コンピュータが理解できる言語、 「プログラミング言語」を話すことが必要です。 世の中には数多くのプログラミング言語があり、それぞれ異なっていて、 そのうちの多くはとても優れたものです。 このチュートリアルでは、その中で、私の好きな言語である Ruby を選びました。 Rubyは私が好きな言語というだけではなくて 今まで数多くの言語を見て来た中で最も容易な言語といえます。 実際、このチュートリアルを書いている本当の理由はこれなのです。 チュートリアルを書こうと決めてから私の好きな言語のRubyを選んだ、 のではなくて、Rubyが簡単であるのを知り、これを使ったプログラミング初心者用の チュートリアルがあるべきだと思って書き始めました。 つまり、このチュートリアルを書こうと思ったのはRubyの単純明快さゆえであって、 私がこの言語を好きだか
未来のプログラマのためのチュートリアル 目次 00. はじめに 01. 数(number) 02. 文字列(string) 03. 変数と代入 04. 数と文字列の変換 05. メソッド(method) 06. 制御構造 07. 配列とイテレータ 08. メソッドの作り方 09. クラス 10. ブロックと手続きオブジェクト 11. このチュートリアルを超えて このチュートリアルについて...
Menu Menu Mac OS X? 漢なら、ターミナルでUTF-8で zsh + vi だろ? というか、プログラミングは、まだしも、サーバメンテでは必須。Terminal.app でもいいけど、xterm 使ってみよう。 X11.app OS のインストール時に忘れずに選択してください。忘れた? OS のメディアから、もう一度入れることができます。 uim uxterm に export XMODIFIERS='@im=uim' を入れます。 http://code.google.com/p/uim/ なのですが、Mac 用は http://code.google.com/p/macuim/ こちら。これを入れてからシステム環境設定側から設定します。 ~/.xinitrc ~/.xresources を使ってください。 uxterm xterm のutf-8用 shell scrip
Shinji KONO / Sat Jul 10 10:05:47 2021
Menu Menu UNIXでは、stat() (あるいは、lstat(),fstat() )システム・コールを用いてファイルの属性(ファイルの管理情報)を調べることができる。ファイルの属性を調べ、画面に出力するプログラムをstat.c に示す。 /* stat.c -- stat システム・コールのシェル・インタフェース $Header: /home/h1/yas/slab-info1-os/4-file/RCS/stat.c,v 1.2 1995/05/31 11:43:32 yas Exp $ Start: 1995/03/07 20:59:12 */ #include <sys/types.h> #include <sys/stat.h> #include <stdio.h> main( argc,argv ) int argc ; char *argv[] ; { if( arg
Menu Menu 1. 目的 この実験では、軽量プロセスを用いて、基本的なプロセス間の同期について学ぶ。C言語によりセマフォを用いるプログラムを作成する。 2. 関連科目 情204 オペレーティング・システム 必修2単位 3. 準備 プロセス間の同期とプロセス間通信の概念をつかみなさい。プロセス間の同期と通信に関する次のキーワードの意味を調べなさい。 相互排除 (mutal exclusion ) セマフォ、計数セマフォ、P命令、V命令 (semaphor) 生産者消費者問題 (producer consumer problem ) 軽量プロセスとコルーチン (light weight process, co-routine ) プロセス切り替え (コンテキスト切り替え) (context switch) 横取り (preemptive ) バリア同期 通常の重いプロセスの場合は、以下の
Operating System の授業 教科書 Operating System Concepts, 10th Edition ソースコードは、Mercurial repository を 学科指定の場所に作ること。元のrepositoryを clone して、そこから変更し commit する。それを scp で置く。その時に、僕から読める permission に指定すること。 課題は補講と競合しないように10/13以降に提出してください。先行して提出しても問題が変更される場合があります。 OSで使用するソフトウェアのinstall os01 Introduction オペレーティングシステムの概要 / File System, ファイルシステム os02 File System, ファイルシステム の続き os03 Process プロセス os04 スケジューリング os05 軽
河野真治 (こうのしんじ) のホームページにようこそ 論文リスト 時相論理に関する研究 講義のページ 発表 ソフトウェアのページ Agda 入門 他には... blog nkf (network kanji filter) に関すること 学内向け案内 (アクセス制限あり) イベント及び写真集 カレーのページ 沖縄に関すること fjに関すること HTMLの例題 (non frame version) (ここはフレームの方が便利) 河野真治について 琉球大学情報工学科 並列信頼研究室 昔の話題 sfの話題 その他の話題 R.I.P. English Page is here メールはこちらへ。kono@ie.u-ryukyu.ac.jp http://bw-www.ie.u-ryukyu.ac.jp/~kono
次のページ
このページを最初にブックマークしてみませんか?
『Shinji Kono's Home Page』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く