Category product ←まだこんなところだったりする
"Category products of a given family of objects is unique up to isomorphism."
嘘ぉ。これどうなん?
GIMP で矢印つき曲線の描き方がわからんので、超落描きスマソ。こういうきれいな図は何で書いてるのかな。
要するに AxB が「本物の」A, B の product で、a, b が射影射 (…なんて言うのか? Projection morphism を直訳してみた)。で、X も product の条件を満たしている、と。そこで X, AxB の間にはどっち方向にも射が存在しなくてはならないので、それが f, g。
追記: 誤解を招いたので補足。「X, AxB の間には最低限 f,g が存在しなくてはならない」→「f, g 以外に X, AxB 間に射が存在しない状況を考える。」上に図示した圏では、恒等射以外に省略されている射は存在しないものとしてるつもり。
"Unique up to isomorphism" ならばこれで になるはず。しかしここで i:X->X が id とは別に存在すると仮定する。それは
となる以外は
と同じであるとする。
追記: i.i = i
そして f.g = i と定義すると、残りの合成射は簡単に定義できていって、結合律とかちゃんと満たすような気がする。しかしそうなると f, g は互いに逆射ではないので (f.g が id じゃないから)、いずれも同型射ではないはず。
何か間違ってるんだろうか。間違ってるんでしょうな。でもどこかわからない。わざわざ結合律とか検証するために script を書いてみたんだけど、確かに圏であるという結果が出てしまった。こういうときは何か恐ろしく基本的な物事を見過ごしてるもんだけど…
ところでその script を練習として haskell で書いたんだけど、自分で目を覆わんばかりに汚くなった。晒しとけば何か助言とか来ないかなー:
-- Debug print とかそのまま
import List
import Maybe
import Char
--- Types
type Symbol = String
data Arrow = Arrow { name :: Symbol,
dom :: Symbol,
cod :: Symbol }
deriving Eq
instance Show Arrow where
show arr = name arr ++ ":" ++ dom arr ++ "->" ++ cod arr
data Arrow_pat = Wildcard
| Set { elms :: [Arrow] }
| Negset { elms :: [Arrow] }
deriving Eq
instance Show Arrow_pat where
show (Set (elm:[])) = name elm
show (Set elms) = "{" ++ concat (intersperse ", " $ map name elms) ++ "}"
show _ = ""
data Composite_arrow = Lhs | Rhs | Fixed Arrow
deriving Eq
instance Show Composite_arrow where
show Lhs = "(<)"
show Rhs = "(>)"
show (Fixed arr) = name arr
matches :: Arrow -> Arrow_pat -> Bool
matches a Wildcard = True
matches a (Set p) = a `elem` p
matches a (Negset p) = not $ a `elem` p
data Rule = Rule { lhs :: Arrow_pat,
rhs :: Arrow_pat,
res :: Composite_arrow }
deriving Eq
instance Show Rule where
show r = foldl1 (++) [show (lhs r), " . ", show (rhs r),
" = ", show (res r)]
applicable :: Rule -> Arrow -> Arrow -> Bool
applicable r left right = (matches left $ lhs r) && (matches right $ rhs r)
apply :: Rule -> Arrow -> Arrow -> Arrow
apply (Rule _ _ Lhs) left _ = left
apply (Rule _ _ Rhs) _ right = right
apply (Rule _ _ (Fixed arr)) _ _ = arr
first = fst
second = snd
third = snd . snd
make_map :: Rule -> Arrow -> Arrow -> (Arrow, Arrow, Arrow)
make_map (Rule _ _ x) l r = case x of
Fixed y -> (l, r, y)
Lhs -> (l, r, l)
Rhs -> (l, r, r)
trim :: String -> String
trim = reverse . triml . reverse . triml
where
triml (c:cs) | isSpace c = triml cs
triml x = x
infix |->
(f, g) |-> (x, y) = (f x, g y)
infixr /-
f /- (x, y) = (f x, f y)
--- Reading input strings
read_rule :: String -> [Arrow] -> Rule
read_rule str arrs = Rule f g h
where (comp, nh) = trim /- split_at '=' str
(f, g) = read_arr_pat arrs /- trim /- split_at '.' comp
h = read_comparr arrs nh
read_arr_pat :: [Arrow] -> String -> Arrow_pat
read_arr_pat arrs "*" = Wildcard
read_arr_pat arrs ('!':str) = Negset $ elms $ read_arr_pat arrs str
read_arr_pat arrs str =
Set $ map (find_by_name arrs . trim) $ split_at_all ',' str
find_by_name :: [Arrow] -> String -> Arrow
find_by_name arrs str = fromJust $ find ((str ==) . name) arrs
read_arrow :: String -> Arrow
read_arrow str = let (n, dc) = trim /- split_at ':' str
(d, c) = trim /- split_at_seq "->" dc
in Arrow n d c
read_comparr :: [Arrow] -> String -> Composite_arrow
read_comparr arrs "$<" = Lhs
read_comparr arrs "$>" = Rhs
read_comparr arrs str = Fixed $ find_by_name arrs str
read_data :: ([String], [String]) -> ([Arrow], [Rule])
read_data (arr_strs, rul_strs) = (arrows, rules)
where
arrows = uniq (eqf name) $ gen_id $ map read_arrow arr_strs
rules = map (flip read_rule arrows) rul_strs
---- Utilities
split_at :: Eq a => a -> [a] -> ([a], [a])
split_at s xs = case (takeWhile (s /=) xs, dropWhile (s /=) xs) of
(bef, []) -> (bef, [])
(bef, _:aft) -> (bef, aft)
split_at_all :: Eq a => a -> [a] -> [[a]]
split_at_all s [] = []
split_at_all s xs = chunk : split_at_all s xs'
where (chunk, xs') = split_at s xs
-- DOTO: optimize with KMP (maybe)
split_at_seq :: Eq a => [a] -> [a] -> ([a], [a])
split_at_seq ss [] = ([], [])
split_at_seq ss xs
| ss `isPrefixOf` xs = ([], xs \\ ss)
| otherwise = let (bef, aft) = split_at_seq ss $ tail xs
in (head xs : bef, aft)
gen_id ls = (map id_for $ uniq (eqf dom) ls) ++ ls
where
id_for (Arrow _ d _) = Arrow ("id_" ++ d) d d
eqf f = (. f) . (==) . f
uniq eq [] = []
uniq eq (x:xs) = x : (uniq eq $ filter (not . eq x) xs)
---- Checks
categoryp :: ([Arrow], [Rule]) -> IO ()
categoryp (arrs, rules) = do
putStr "Closed under composition: "
print $ all definedp composable_pairs
putStr "Associative composition: "
print $ all assocp composable_triples
putStr "times table:\n"
putStr $ concatMap (\(f, g) -> concat [name f, ".", name g, "=",
name $ f /./ g, "\n"])
composable_pairs
putStr "\n\nassociation table:\n"
putStr $ concat $ intersperse "\n" $ map dump composable_triples
where
dump (f, g, h)
= concat
[name f, ".", name g, ".", name h, "-->",
"\t",
name (f /./ g), ".", name h, "=", name $ fromMaybe a lassoc,
"\t",
name f, ".", name (g /./ h), "=", name $ fromMaybe a rassoc]
where lassoc = f `compose` g >>= (`compose` h)
rassoc = g `compose` h >>= (f `compose`)
a = Arrow "nil" "" ""
infix /./
f /./ g = fromMaybe a $ compose f g
composable_pairs = [(f, g) | f <- arrs, g <- arrs, dom f == cod g]
composable_triples = [(f, g, h) |
(f, g) <- composable_pairs, h <- arrs,
dom g == cod h]
definedp operands
= isJust $ (uncurry compose) operands
assocp (f, g, h)
= let lassoc = f `compose` g >>= (`compose` h)
rassoc = g `compose` h >>= (f `compose`)
in if lassoc == rassoc
then True
else error $ foldl1 (++)
[name f, " . ", name g, " . ", name h,
" could be ", name $ fromJust lassoc,
" or ", name $ fromJust rassoc]
infer, compose :: Arrow -> Arrow -> Maybe Arrow
compose f g
= case filter (\r -> applicable r f g) rules of
[] -> infer f g
[r] -> Just $ apply r f g
_ -> error $ show f ++ " . " ++ show g ++ " ambiguous"
infer f g
| "id_" `isPrefixOf` name f = Just g
| "id_" `isPrefixOf` name g = Just f
| otherwise
= case filter (\a -> dom a == dom g
&& cod a == cod f) arrs of
[arr] -> Just arr
_ -> error $ show f ++ " . " ++ show g ++ " not defined"
matches_rule (f, g) rule
= (matches f $ lhs rule) && (matches g $ rhs rule)
main = getContents
>>= return . split_at "" . lines
>>= (\x -> print x >> return x)
>>= return . read_data
>>= categorypとりあえずこれぐらいの program で Arrow なんて作ったのがよくなかったかもな。不便ぢゃ。あと、高階関数の使いどころがよくわからん。そして "〜not defined" とか error を出してる所の大半は本当は警告を出力して処理を続行したいが、どうやったらいいかわからない。
入力 file:
f : AxB -> X g : X -> AxB p1 : AxB -> A p2 : AxB -> B q1 : X -> A q2 : X -> B i : X -> X x : X -> C y : X -> C h : AxB -> C f . g = i g . f = id_AxB i . !id_X = $> !x,i,id_X . i = $< x . i = y h . g = y
