Agda + Lattice + Poset

ひさしぶりにagdaを触ってみた．
コンパイラと標準ライブラリを最新版に更新して，あちこち眺めた．
コンパイラが2Gのメモリを食い潰すくらいに標準ライブラリが充実してきているみたい．
Equational Reasoningができるようになっているらしい．

試しに見よう見まねで束から半順序を作ってみた．

LatticePoset.agda

open import Algebra

module LatticePoset (L : Lattice) where
open Lattice L

open import Relation.Binary
open import Algebra.Props.Lattice
open import Data.Product

import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid

_≤_ : Rel carrier
x ≤ y = x ∨ y ≈ y

_≤'_ : Rel carrier
x ≤' y = x ∧ y ≈ x

infix 4 _≤_ _≤'_

≤-≤'-inc : ∀ {x y} → x ≤ y → x ≤' y
≤-≤'-inc {x} {y} p = begin
  x ∧ y ≈⟨ ∧-pres-≈ refl (sym p) ⟩
  x ∧ (x ∨ y) ≈⟨ proj₂ absorptive x y ⟩
  x ∎

≤'-≤-inc : ∀ {x y} → x ≤' y → x ≤ y
≤'-≤-inc {x} {y} p = begin
  x ∨ y ≈⟨ ∨-pres-≈ (sym p) refl ⟩
  (x ∧ y) ∨ y ≈⟨ ∨-comm (x ∧ y) y ⟩
  y ∨ (x ∧ y) ≈⟨ ∨-pres-≈ refl (∧-comm x y) ⟩
  y ∨ y ∧ x ≈⟨ proj₁ absorptive y x ⟩
  y ∎

≤-refl : _≈_ ⇒ _≤_
≤-refl {x} {y} p = begin
  x ∨ y ≈⟨ ∨-pres-≈ p refl ⟩
  y ∨ y ≈⟨ ∨-idempotent L y ⟩
  y ∎

≤-trans : Transitive _≤_
≤-trans {x} {y} {z} p q = begin
  x ∨ z ≈⟨ ∨-pres-≈ refl (sym q) ⟩
  x ∨ (y ∨ z) ≈⟨ sym (∨-assoc x y z) ⟩ 
  (x ∨ y) ∨ z ≈⟨ ∨-pres-≈ p refl ⟩
  y ∨ z ≈⟨ q ⟩
  z ∎

≤-resp-≈ : _≤_ Respects₂ _≈_
≤-resp-≈ = (λ {x} {y} {z} p q → begin x ∨ z ≈⟨ ∨-pres-≈ refl (sym p) ⟩
                                      x ∨ y ≈⟨ q ⟩
                                      y ≈⟨ p ⟩
                                      z ∎) ,
           λ {x} {y} {z} p q → begin z ∨ x ≈⟨ ∨-pres-≈ (sym p) refl ⟩
                                     y ∨ x ≈⟨ q ⟩
                                     x ∎

≤-antisym : Antisymmetric _≈_ _≤_
≤-antisym {x} {y} p q = begin
  x ≈⟨ sym q ⟩ 
  y ∨ x ≈⟨ ∨-comm y x ⟩
  x ∨ y ≈⟨ p ⟩
  y ∎

≤-isPreorder : IsPreorder _≈_ _≤_
≤-isPreorder = record {
                 isEquivalence = isEquivalence;
                 reflexive = ≤-refl;
                 trans = ≤-trans;
                 ∼-resp-≈ = ≤-resp-≈
               }

≤-isPartialOrder : IsPartialOrder _≈_ _≤_
≤-isPartialOrder = record {
                     isPreorder = ≤-isPreorder;
                     antisym = ≤-antisym
                   }

LatticePoset : Poset
LatticePoset = record {
                 carrier = carrier;
                 _≈_ = _≈_;
                 _≤_ = _≤_;
                 isPartialOrder = ≤-isPartialOrder
               }

twitter投稿スクリプト

今日の（ほぼ）一行スクリプト

http://www.oceans.mydns.jp/memo/20090506001.htm を参考にtwitterの投稿スクリプトを書いてみた。
パスワードが平文で保存されているのはちょっときもちわるい。

uri-encode

#!/usr/bin/ruby -n
require "cgi"
print CGI.escape($_)

uri-decode

#!/usr/bin/ruby -n
require "cgi"
print CGI.unescape($_)

twitter-post

#!/bin/sh
wget --post-data="status=`echo $@ | nkf -w | uri-encode`" \
 --http-user=tzik_tack \
 --http-password=`cat ~/repos/private/passwd/twitter` \
 --no-check-certificate https://twitter.com/statuses/update.xml \
 -O /dev/null

grub + dvorak

以前書いた /boot/grub/menu.lst はメモるに値すると判断した。
grubのメニューでキー配列をdvorak (us) にし、CtrlとCaps Lockを入れ替える。
（あんまり使わないけど）これでブートメニューでもdvorak。

setkey control capslock
setkey capslock control

setkey bracketleft minus
setkey bracketright equal

setkey quote q
setkey comma w
setkey period e
setkey p r
setkey y t
setkey f y
setkey g u
setkey c i
setkey r o
setkey l p
setkey slash bracketleft
setkey equal bracketright

#setkey a a
setkey o s
setkey e d
setkey u f
setkey i g
setkey d h
setkey h j
setkey t k
setkey n l
setkey s semicolon

setkey minus quote
setkey semicolon z
setkey q x
setkey j c
setkey k v
setkey x b
setkey b n
#setkey m m
setkey w comma
setkey v period
setkey z slash

setkey braceleft underscore
setkey braceright plus

setkey doublequote Q
setkey less W
setkey greater E
setkey P R
setkey Y T
setkey F Y
setkey G U
setkey C I
setkey R O
setkey L P
setkey question braceleft
setkey plus braceright

#setkey A A
setkey O S
setkey E D
setkey U F
setkey I G
setkey D H
setkey H J
setkey T K
setkey N L
setkey S colon
setkey underscore doublequote

setkey colon Z
setkey Q X
setkey J C
setkey K V
setkey X B
setkey B N
#setkey M M
setkey W less
setkey V greater
setkey Z question

ghostscriptの日本語化

いつのまにか，二ヶ月半も放置していたことに愕然とした．

長いことghostscriptの文字化けを解消できなかったが，
さっきやっとうまくできた．

/usr/share/ghostscript/8.64/Resource/Init/cidfmap
に
/ipam << /FileType /TrueType /Path (/usr/share/fonts/ja-ipafonts/ipam.otf) /CSI [(Japan1) 6] >> ;
/ipag << /FileType /TrueType /Path (/usr/share/fonts/ja-ipafonts/ipag.otf) /CSI [(Japan1) 6] >> ;
/Ryumin-Light /ipam
を追加．

これでasymptoteの文字化けを解消し，
図中で日本語を使えるようになった．

パソコン買い替えた

今サーバとして動かしてるマシンが窮屈になってきたので買い替えてみた．Faithの組立キットを通販購入．
発送まで8営業日ほどで，受け取りは土日指定にした．再来週の末には届くかな．

スペックはこんなかんじ．
HDDを大きめのに，CPUをL2キャッシュが多めのに換装した．
LANが100BASEなのがちょっと気になる．
LAN越しにバックアップを取るときとかに時間がかかりそう．
音と映像はきにしない．

値段は 33,700円 + 13,500円×1.05 = 47,875円なり．貧乏学生には割と痛い出費…．