僕は、朝8時に起きる。まずは PC を起動して、水とコーヒーを飲む。そして、たばこを吸う。
朝食は、簡単なパンやカロリーメイトを食べ、ヤクルトを飲む。午前中は、PC でブログ巡回や 5ch をしながら過ごす。
昼食は、昨日の残り物を食べるか、外でテイクアウトをする。午後は、数学やプログラミングの研究活動をしたり、将棋中継を見たりする。昼寝をすることもある。
基本的には、外出はしない。たまに、買い物や散歩に行く程度だ。
夕食は、それなりに食べる。夕食を食べると眠くなるので、20時ごろには寝る。たまに、夜中に起きて活動しているときもある。
僕は、数学とプログラミングが大好きだ。毎日、数学やプログラミングの研究活動をすることで、充実感を得ている。
将棋も大好きだ。将棋中継を見ると、時間を忘れて見入ってしまう。
僕の一日はとても単調かもしれない。でも、僕はこれで満足している。この生活が、僕には合っている。
僕は、自分のペースで生きていきたいと思っている。僕は、自分の好きなことを好きなだけしたいと思っている。僕は、自分の人生を自分の思い通りに生きていきたいと思っている。
人間はミスをする生き物だ。
医療 AI による診断
インフラ
自動運転
金融 意思決定の多くをコンピュータに任せて経済が動いている
人間の仕事ほとんど全てに、機械・AI のアシストがつく。
どうだろう。
失敗ができなくなる未来がやってくるかもしれない。
特におちは無いです。
大木ゆきの氏
こーへ氏
中島義道氏
https://twitter.com/yoshimichi_bot（非公式）
大木ゆきの氏 ー こーへ氏 ー 中島義道氏
共通項 お手上げ ー 全部投げる ー <半分>降りる
そのあと 幸せになる ー なにもしない、真実、無 ー 死について考える
19/10/02追記
PCが壊れたので再度設定した。
-- ----------
- 初回起動
- 無線LAN接続
- タスクバーの設定
- スリーブにしない
- パフォーマンスを優先
- 仮想メモリを0MBにする
- エクスプローラー
- 拡張子を表示する
- 隠しファイルを表示する
- ピクチャなどのフォルダをEドライブに
- FireFox
- 規定のブラウザにする
- 新しいタブで、すぐ
- Firefox を閉じたときに Cookie とサイトデータを削除する
YouTube, Twitter, pixiv, abemaは許可
- about:config browser.urlbar.trimURLs
- スーパーセキュリティ
- Jane Style
http://dobonkai.hatenablog.com/entry/Jane-Style
http://usbcafe.blog111.fc2.com/blog-entry-60.html
いらないかhttps://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q11181622636
- Clibor
- スタートアップへ登録 shell:startup
- Tablacus Explorer
- Lhaplus
- TTClock
年と曜日を表示
- めもりくりーなー ×
セキュリティチェックに引っかかった
- thilmera 7
これはすばらしい
- ふせん
- セーフモード
bcdedit /set {default} bootmenupolicy legacy
- 回復ドライブ
作成
- 共有フォルダ
- https://www.blockmodule.com/archives/2874
次の日開通？ うまくいかなかったのでIP直打ち
- Schedule Watcher
時報 C:\Windows\Media
- VSCode
- 日本語化
- 階層リンクを表示しない
- workbench.editor.enablePreviewをFalse
- **/*.ibc
- files.eol
- zenkaku
- オートインデントを使わない
- 「CTRLキー+ホイール」でテキストフォントの拡大・縮小を設定
- haskell-linter
- C:\Users\furuta5\AppData\Roaming\local\bin\hlint.exe
- onSave
- stack
- E:\Users\furuta5\AppData\Roaming\local\bin
Eドライブにしたのは失敗
- stack install primes OK
- stack install hlint → chcp 65001で2回目でok
- Egison stackで 3.9.1
- Idris バイナリで 1.3.2
- Rust インストーラで
https://visualstudio.microsoft.com/ja/downloads/?rr=https%3A%2F%2Fwww.rust-lang.org%2Fen-US%2Finstall.html
- Agda
https://ameblo.jp/righ1113/entry-12218319376.html
- 設定
C:\Users\furuta5\AppData\Roaming\.spacemacs
- helmの下にagdaと書く
- その下のauto-completionを有効にする
- 画面サイズ
(defun dotspacemacs/user-init ()
;; 初期Frameサイズを指定
(setq inhibit-startup-screen t)
(setq initial-frame-alist
'((top . 30) (left . 370) (width . 160) (height . 45))
)
)
- フォントサイズ
C:\Users\furuta5\AppData\Roaming\.emacs.d\init.el
の (spacemacs/init)の下に (dotspacemacs/init)を追加
https://ics.media/entry/7010/
dotspacemacs-default-font '("DejaVu Sans"
:size 16
:weight normal
:width normal
:powerline-scale 1.1)
SPC f f ファイルを開く
yy 一行コピー
p ペースト
u アンドゥ
SPC w / ウィンドウを垂直分割
:w 保存
C-x <Enter> f で Unix
C-x C-0 + C-g フォントサイズ大ぼつ
ctrl c ctrl h
ctrl c ctrl ,
, g g go to difinition
, g G back
- GeoGebra
やってない...
- CPL
GitHubからクローンして、stack run cpl
cabal使っちゃいかんよ
- Anaconda
Jupyterも入っているPython
https://qiita.com/t2y/items/2a3eb58103e85d8064b6
https://qiita.com/surei/items/9f25d7efa7c67d55d98f
http://onoz000.hatenablog.com/entry/2018/02/11/142347
- conda createで仮想環境を作る
- 目的のフォルダ内で←これ違う
conda create -n py37 Anaconda
- 仮想環境の確認
conda info -e
- conda activate py37で、環境をActiveにする
- conda deactivateで非アクティブにする
やはりWindowsではJupyterでEgisonは動かなかった
- Windows Subsystem for Linux
https://qiita.com/hiiragi1104/items/c2e9042bc6170873a859
VSCodeを使ってコードを書こう
homebrewは失敗
https://nakomii.hatenablog.com/entry/wsl_ubuntu
$ echo 'export DISPLAY=localhost:0.0' >> ~/.bash_profile
$ source ~/.bash_profile
これも失敗
- VirtualBox
インストール後
sudo apt update
sudo apt upgrade
sudo apt install cabal-install
cabal update
cabal install egison-3.9.4 3.8.0でも良いか stackでEgison入れても良いかもね
.bashrcに
export PATH=${PATH}:/home/furuta5/.cabal/bin
sudo apt install python3-pip
sudo apt install git
適当なフォルダで
git clone https://github.com/egison/egison_kernel
cd egison_kernel
pip3 install .
python3 -m egison_kernel.install
pip3 install tornado==5.1.1
pip3 install jupyter
cd
cd egison
egison.jsを持ってくる
jupyter notebook
/home/furuta5/.local/share/jupyter に呼び出しjsonがあるよ
VirtualBoxのUbuntu ファイル・アプリを起動し、
Ctrl + h で隠しファイル・隠しフォルダ(ディレクトリ)を表示することができます。
- Windows Subsystem for Linux
*PCを消して点けたら起動しない*
https://www.petitmonte.com/windows/wsl_not_start.html
https://www.atmarkit.co.jp/ait/articles/1903/18/news031.html
Ubuntu 18.04 LTSを入れる
VSCodeにもなんか自動で入る
bashで
sudo apt update
sudo apt upgrade
sudo apt install cabal-install
cabal update
cabal install egison-3.9.4
sudo apt install python3-pip
--
pip3 install numpy
pip3 install scipy
pip3 install matplotlib
pip3 install Pillow
pip3 install ipython[all]
--
pip3 install tornado==5.1.1
.bashrcに
export PATH=${PATH}:/home/furuta5/.cabal/bin:/home/furuta5/.local/bin
pip3 install jupyter
-- ----------
デスクトップPCを買い替えた。
新しいPCにすると、設定する事がたくさんあるので、書き留めておこう。
-- ----------
- 初回起動
- 無線LAN接続
- エクスプローラー
- 拡張子を表示する
- 隠しファイルを表示する
- ピクチャなどのフォルダをEドライブに
- タスクバーの設定
- 壁紙変更
- スリーブにしない
- パフォーマンスを優先
- 仮想メモリを0MBにする
- shortcutフォルダにパスを通す
- [Win] + r -> shell:startup
- FireFox
- 規定のブラウザにする
- 新しいタブで、すぐ
- 終了時に履歴を消去する キャッシュとクッキー
- ブックマークをインポート
- browser.urlbar.trimURLs
- 共有フォルダ
- https://www.blockmodule.com/archives/2874
- Cliborをshareから移す
- スタートアップへ登録
- VSCode
- 日本語化
- 階層リンクを表示しない
- workbench.editor.enablePreviewをFalse
- Monokai Pro いらなかった
- **/*.ibc
- files.eol
- zenkaku
- オートインデントを使わない
- 「CTRLキー+ホイール」でテキストフォントの拡大・縮小を設定
- haskell-linter
- C:\Users\furuta5\AppData\Roaming\local\bin\hlint.exe
- onSave
- Lhaplus
- Tablacus Explorer
- ふせん
- スーパーセキュリティ
- Jane Style
- Schedule Watcher
- めもりくりーなー
- GitHub Desktop
- TTClock
- stack
- C:\Users\furuta5\AppData\Roaming\local\bin
- stack install primes OK
- stack install hlint ダメだった → chcp 65001で解決
- stack install cabal-install ダメだった
- hie ダメだった
- MSYS2 ぼつ /c/Windows/System32/chcp.com 932
- Egison stackで
- Idris バイナリで
- Git
- df
- Isabelle
- ExcelとWord
-- ----------
ソースコードは以下。
-- -----
-- hintパッケージをインストールする
module Godel03 where
import qualified Language.Haskell.Interpreter as I
import Control.Monad.Fix
import System.IO.Unsafe
g = const "unprovable const id () $ (\\x -> x ++ show x) \"unprovable const id () $ (\\\\x -> x ++ show x) \""
evalStr str = I.runInterpreter $ do
I.setImports ["Prelude"]
I.eval str
eval str = unsafePerformIO $ do
result <- evalStr str
case result of
Right r -> return r
Left er -> return "error"
-- -----
実行結果。
*Godel03> show $ g (fix g)
"\"unprovable const id () $ (\\\\x -> x ++ show x) \\\"unprovable const id () $ (\\\\\\\\x -> x ++ show x) \\\"\""
*Godel03> eval $ drop 11 $ g (fix g)
"\"unprovable const id () $ (\\\\x -> x ++ show x) \\\"unprovable const id () $ (\\\\\\\\x -> x ++ show x) \\\"\""
*Godel03> (show $ g (fix g)) == (eval $ drop 11 $ g (fix g))
True
「g (fix g)」は、（文字列だが）ある値がunprovable証明不能だと言っている。
ある値が何かと、evalすると、元の文字列が出てきた。
つまり、「g (fix g)」は「私はunprovable証明不能です」と言っていることになる。
以上が不完全性定理の（一部の）説明です。
停止性問題に関して、Schemeでやってる記事を見つけた。
パーフェクトだと思った。
さあみんなもRacketとかで実行しよう！
これをHaskellで出来ないかと思った。
作ったのが以下。
-- -----
module Halt01 where
turing x =
if halt x x then last $ repeat "inf" else "done"
turing' = turing
halt turing turing' = False
-- -----
これを実行すると以下のようになる。
C:\me\Haskell\Godel>ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :l Halt01
[1 of 1] Compiling Halt01 ( Halt01.hs, interpreted )
Ok, modules loaded: Halt01.
*Halt01> halt turing turing
False
*Halt01> turing turing
"done"
これは、「turing turing」が止まらないと言っているのに、
実際に「truing turing」を実行すると、止まるのだ。
ソースコードをhalt turing turing' = Truｅに変えると、以下のようになる。
*Halt01> halt turing turing
True
*Halt01> turing turing
"（無限ループ）
これは、「turing turing」が止まると言っているのに、
実際に「truing turing」を実行すると、止まらないのだ。
つまり、関数の停止性を判定する「halt」は作れないということだ。
それにしても型付きのHaskellで「turing turing」とか出来るんですね。
CoqやAgdaじゃできないだろうな。
