K&R Cの付録Aの文法(ANSI Cの文法?)で直接左再帰除去で対応出来ない左再帰な非終端記号があるかどうか調べる 

import qualified Data.Set as Set
import qualified Data.List as List

data EBNF =
    Seq EBNF EBNF |
    Choice EBNF EBNF |
    Opt EBNF |
    Terminal String | -- ただし空文字列禁止
    NonTerminal NT
    deriving (Show , Eq , Ord)
    
{- 手間なので、型シノニムで -}
type HandleEmpty = Bool {- True = Accept , False = Reject -}
{-
Acceptは、その式が空文字列を受理出来るという事をあらわす
一方Rejectは、その式は空文字列を受理しないという事をあらわす
-}
             
{-
与えられたEBNFの部分式すべてからなる集合を求める。
自分自身も部分式であるとする。
-}
subexps :: EBNF -> Set.Set EBNF
subexps s@(Seq a b) = Set.insert s (Set.union (subexps a) (subexps b))
subexps s@(Choice a b) = Set.insert s (Set.union (subexps a) (subexps b))
subexps s@(Opt a) = Set.insert s (subexps a)
subexps s@(Terminal str) = Set.singleton s
subexps s@(NonTerminal nt) = Set.singleton s

{-
こいつをぶん回す。
accept_setは現段階で判明している、空文字列を受理する式
reject_setは現段階で判明している、空文字列を受理しない式
-}
data Handles = MkHandle { accept_set :: Set.Set EBNF , reject_set :: Set.Set EBNF }
             deriving (Show , Eq)

{-
現在分かっていること(=Handles)から、
今注目しているEBNFの式が、空文字列を受理するか、しないかを調べて更新
-}
deriv :: EBNF -> Handles -> Handles
deriv exp@(Seq a b) self@(MkHandle accept reject)
    | (Set.member a reject || Set.member b reject) = MkHandle accept (Set.insert exp reject)
    | (Set.member a accept && Set.member b accept) = MkHandle (Set.insert exp accept) reject
    | otherwise = self
deriv exp@(Choice a b) self@(MkHandle accept reject)
    | (Set.member a accept || Set.member b accept) = MkHandle (Set.insert exp accept) reject
    | (Set.member a reject && Set.member b reject) = MkHandle accept (Set.insert exp reject)
    | otherwise = self
deriv exp@(Opt e) (MkHandle accept reject) = MkHandle (Set.insert exp accept) reject
deriv exp@(Terminal str) (MkHandle accept reject) = MkHandle accept (Set.insert exp reject)
deriv exp@(NonTerminal nt) self@(MkHandle accept reject)
    | Set.member (grammer nt) accept = MkHandle (Set.insert exp accept) reject
    | Set.member (grammer nt) reject = MkHandle accept (Set.insert exp reject)
    | otherwise = self

all_nt :: [NT]
all_nt = enumFrom (toEnum 0)

{-
grammber_subexpsは、
{ 文法中の非終端記号 } u { 各非終端記号の生成規則に対する部分式からなる集合 }
-}
grammer_subexps = Set.union
                  (foldr (\e acc -> Set.union (subexps $ grammer e) acc) Set.empty all_nt)
                  (Set.fromList $ map NonTerminal all_nt)

{-
fixpointで判別付かなかった非終端記号に関しては、
その非終端記号から、
空文字列の受理をする、もしくは受理しないといった部分式に到達しない
無限回の導出が出来るため、左再帰を求める計算の上ではRejectと見ても良い。

計算的な意味としては、入力に対する無限の導出となって停止しない為、
後に出てくるleft cornerの考え的にはRejectと言えるということになります。

例えば、
S = A S
A = B
B = A
この例だとA,B,S全ての非終端記号の判断はつきません。
なので、全て空文字列を受理しないとして扱います。
-}
grammer_handles =
    foldr (\e self@(MkHandle accept reject) ->                             
               case Set.member e accept ||
                    Set.member e reject of
                 True -> self
                 False -> MkHandle accept (Set.insert e reject)) res (map NonTerminal all_nt)
  where
    {-
      fixpointは、文法中に出現する全ての部分式について、
      それが空文字列を受理するか受理しないかを分類する計算。
      
      かならず停止する。
     -}
    fixpoint cur =
        case cur == res of
          True -> res
          False -> fixpoint res
        where
          res = Set.fold deriv cur grammer_subexps
    
    res  = fixpoint (MkHandle Set.empty Set.empty)


(./) a b = Choice a b
(.>) a b = Seq a b
op a = Opt (NonTerminal a)
opt a = Opt a
t a = Terminal a
nt a = NonTerminal a

infixr 1 ./
infixr 2 .>

direct_left_recursion :: NT -> [NT]
direct_left_recursion e = collect $ grammer e
    where
      collect :: EBNF -> [NT]
      collect (Seq (Opt a) b) = (collect a) ++ (collect b)
      collect (Seq a b) = (collect a)
      collect (Choice a b) = (collect a) ++ (collect b)
      collect (Opt e) = []
      collect (Terminal _) = []
      collect (NonTerminal nt) | e == nt = [nt]
                               | otherwise = []

{-
ある非終端記号に対して、その生成規則に注目する

その生成規則のうち、入力列の頭にぶつかる可能性のある非終端記号をかき集めてくる

もしこの中に自分自身が含まれる、すなわち
A ∈ direct_left_corner(A)
ならば、Aは左再帰である(直接左再帰とは限らない)
-}
left_corner :: NT -> [NT]
left_corner = lc . grammer
    where
      lc :: EBNF -> [NT]
      lc (Seq a b)
          | Set.member a (accept_set grammer_handles) = (lc a) ++ (lc b)
          | otherwise = lc a
      lc (Choice a b) = (lc a) ++ (lc b)
      lc (Opt e) = lc e
      lc (Terminal _) = []
      lc (NonTerminal nt) = [nt]

collect_left_corner :: Set.Set NT -> Set.Set NT
collect_left_corner s =
  Set.fold (\e acc -> Set.union (Set.fromList $ left_corner e) acc) Set.empty s

mutual_left_corner :: NT -> Set.Set NT
mutual_left_corner nt =
  loop (Set.fromList $ foldr List.delete (left_corner nt) (direct_left_recursion nt))
    where
      loop s =
          case res == s of
            True -> res
            False -> loop res
        where
          res = Set.union s (collect_left_corner s)

is_direct_left_recursion nt = List.elem nt (direct_left_recursion nt)
is_mutually_left_recursion nt = Set.member nt (mutual_left_corner nt)

data NT =
    Translation_unit |
    External_declaration |
    Function_definition |
    Declaration |
    Declaration_list |
    Declaration_specifiers |
    Storage_class_specifier |
    Type_specifier |
    Type_qualifier |
    Struct_or_union_specifier |
    Struct_or_union |
    Struct_declaration_list |
    Init_declarator_list |
    Init_declarator |
    Struct_declaration |
    Specifier_qualifier_list |
    Struct_declarator_list |
    Struct_declarator |
    Enum_specifier |
    Enumerator_list |
    Enumerator |
    Declarator |
    Direct_declarator |
    Pointer |
    Type_qualifier_list |
    Parameter_type_list |
    Parameter_list |
    Parameter_declaration |
    Identifier_list |
    Initializer |
    Initializer_list |
    Type_name |
    Abstract_declarator |
    Direct_abstract_declarator |
    Typedef_name |
    Statement |
    Labeled_statement |
    Expression_statement |
    Compound_statement |
    Statement_list |
    Selection_statement |
    Iteration_statement |
    Jump_statement |
    Expression |
    Assignment_expression |
    Assignment_operator |
    Conditional_expression |
    Constant_expression |
    Logical_OR_expression |
    Logical_AND_expression |
    Inclusive_OR_expression |
    Exclusive_OR_expression |
    And_expression |
    Equality_expression |
    Relational_expression |
    Shift_expression |
    Additive_expression |
    Multiplicative_expression |
    Cast_expression |
    Unary_expression |
    Unary_operator |
    Postfix_expression |
    Primary_expression |
    Argument_expression_list |
    Constant
    deriving (Show , Eq , Ord , Enum)

translation_unit = NonTerminal Translation_unit
external_declaration = NonTerminal External_declaration
function_definition = NonTerminal Function_definition
declaration = NonTerminal Declaration
declaration_list = NonTerminal Declaration_list
declaration_specifiers = NonTerminal Declaration_specifiers
storage_class_specifier = NonTerminal Storage_class_specifier
type_specifier = NonTerminal Type_specifier
type_qualifier = NonTerminal Type_qualifier
struct_or_union_specifier = NonTerminal Struct_or_union_specifier
struct_or_union = NonTerminal Struct_or_union
struct_declaration_list = NonTerminal Struct_declaration_list
init_declarator_list = NonTerminal Init_declarator_list
init_declarator = NonTerminal Init_declarator
struct_declaration = NonTerminal Struct_declaration
specifier_qualifier_list = NonTerminal Specifier_qualifier_list
struct_declarator_list = NonTerminal Struct_declarator_list
struct_declarator = NonTerminal Struct_declarator
enum_specifier = NonTerminal Enum_specifier
enumerator_list = NonTerminal Enumerator_list
enumerator = NonTerminal Enumerator
declarator = NonTerminal Declarator
direct_declarator = NonTerminal Direct_declarator
pointer = NonTerminal Pointer
type_qualifier_list = NonTerminal Type_qualifier_list
parameter_type_list = NonTerminal Parameter_type_list
parameter_list = NonTerminal Parameter_list
parameter_declaration = NonTerminal Parameter_declaration
identifier_list = NonTerminal Identifier_list
initializer = NonTerminal Initializer
initializer_list = NonTerminal Initializer_list
type_name = NonTerminal Type_name
abstract_declarator = NonTerminal Abstract_declarator
direct_abstract_declarator = NonTerminal Direct_abstract_declarator
typedef_name = NonTerminal Typedef_name
statement = NonTerminal Statement
labeled_statement = NonTerminal Labeled_statement
expression_statement = NonTerminal Expression_statement
compound_statement = NonTerminal Compound_statement
statement_list = NonTerminal Statement_list
selection_statement = NonTerminal Selection_statement
iteration_statement = NonTerminal Iteration_statement
jump_statement = NonTerminal Jump_statement
expression = NonTerminal Expression
assignment_expression = NonTerminal Assignment_expression
assignment_operator = NonTerminal Assignment_operator
conditional_expression = NonTerminal Conditional_expression
constant_expression = NonTerminal Constant_expression
logical_OR_expression = NonTerminal Logical_OR_expression
logical_AND_expression = NonTerminal Logical_AND_expression
inclusive_OR_expression = NonTerminal Inclusive_OR_expression
exclusive_OR_expression = NonTerminal Exclusive_OR_expression
and_expression = NonTerminal And_expression
equality_expression = NonTerminal Equality_expression
relational_expression = NonTerminal Relational_expression
shift_expression = NonTerminal Shift_expression
additive_expression = NonTerminal Additive_expression
multiplicative_expression = NonTerminal Multiplicative_expression
cast_expression = NonTerminal Cast_expression
unary_expression = NonTerminal Unary_expression
unary_operator = NonTerminal Unary_operator
postfix_expression = NonTerminal Postfix_expression
primary_expression = NonTerminal Primary_expression
argument_expression_list = NonTerminal Argument_expression_list
constant = NonTerminal Constant

identifier = t "identifier"
string = t "string"
integer_constant = t "integer_constant"
character_constant = t "character_constant"
floating_constant = t "floating_constant"
enumeration_constant = t "enumeration_constant"

grammer Translation_unit =
    external_declaration ./
    translation_unit .> external_declaration
grammer External_declaration =
    function_definition ./
    declaration
grammer Function_definition = opt declaration_specifiers .> declarator .> opt declaration_list .> compound_statement
grammer Declaration = declaration_specifiers .> opt init_declarator_list .> t "!"
grammer Declaration_list =
    declaration ./
    declaration_list .> declaration
grammer Declaration_specifiers =
  storage_class_specifier .> opt declaration_specifiers ./
  type_specifier .> opt declaration_specifiers ./
  type_qualifier .> opt declaration_specifiers
grammer Storage_class_specifier =
    t "auto" ./ t "register" ./ t "static" ./ t "extern" ./ t "typedef"
grammer Type_specifier =
    t "void" ./ t "char" ./ t "short" ./ t "int" ./ t "long" ./ t "float" ./ t "double" ./ t "signed" ./
    t "unsigned" ./ struct_or_union_specifier ./ enum_specifier ./ typedef_name
grammer Type_qualifier = t "const" ./ t "volatile"
grammer Struct_or_union_specifier =
  struct_or_union .> opt identifier .> t "{" .> struct_declaration_list .> t "}" ./
  struct_or_union .> identifier
grammer Struct_or_union = t "struct" ./ t "union"
grammer Struct_declaration_list = struct_declaration ./ struct_declaration_list .> struct_declaration
grammer Init_declarator_list = init_declarator ./ init_declarator_list .> t "," .> init_declarator
grammer Init_declarator = declarator ./ declarator .> t "=" .> initializer
grammer Struct_declaration = specifier_qualifier_list .> struct_declarator_list .> t ";"
grammer Specifier_qualifier_list =
    type_specifier .> opt specifier_qualifier_list ./
    type_qualifier .> opt specifier_qualifier_list
grammer Struct_declarator_list =
    struct_declarator ./
    struct_declarator_list .> t "," .> struct_declarator
grammer Struct_declarator =
    declarator ./
    opt declarator .> t ":" .> constant_expression
grammer Enum_specifier =
    t "enum" .> opt identifier .> t "{" .> enumerator_list .> t "}" ./
    t "enum" .> identifier
grammer Enumerator_list =
    enumerator ./
    enumerator_list .> t "," .> enumerator
grammer Enumerator =
    identifier ./
    identifier .> t "=" .> constant_expression
grammer Declarator = opt pointer .> direct_declarator
grammer Direct_declarator =
    identifier ./
    t "(" .> declarator .> t ")" ./
    direct_declarator .> t "[" .> opt constant_expression .> t "]" ./
    direct_declarator .> t "(" .> parameter_type_list .> t ")" ./
    direct_declarator .> t "(" .> opt identifier_list .> t ")"
grammer Pointer =
    t "*" .> opt type_qualifier_list ./
    t "*" .> opt type_qualifier_list .> pointer
grammer Type_qualifier_list =
    type_qualifier ./
    type_qualifier_list .> type_qualifier
grammer Parameter_type_list =
    parameter_list ./
    parameter_list .> t "," .> t "..."
grammer Parameter_list =
    parameter_declaration ./
    parameter_list .> t "," .> parameter_declaration
grammer Parameter_declaration =
    declaration_specifiers .> declarator ./
    declaration_specifiers .> opt abstract_declarator
grammer Identifier_list =
    identifier ./
    identifier_list .> t "," .> identifier
grammer Initializer =
    assignment_expression ./
    t "{" .> initializer_list .> t "}" ./
    t "{" .> initializer_list .> t "," .> t "}"
grammer Initializer_list =
    initializer ./
    initializer_list .> t "," .> initializer
grammer Type_name =
    specifier_qualifier_list .> opt abstract_declarator
grammer Abstract_declarator =
    pointer ./
    opt pointer .> direct_abstract_declarator
grammer Direct_abstract_declarator =
    t "(" .> abstract_declarator .> t ")" ./
    opt direct_abstract_declarator .> t "[" .> opt constant_expression .> t "]" ./
    opt direct_abstract_declarator .> t "(" .> opt parameter_type_list .> t ")"
grammer Typedef_name = identifier
grammer Statement =
    labeled_statement ./
    expression_statement ./
    compound_statement ./
    selection_statement ./
    iteration_statement ./
    jump_statement
grammer Labeled_statement =
    identifier .> t ":" .> statement ./
    t "case" .> constant_expression .> t ":" .> statement ./
    t "default" .> t ":" .> statement
grammer Expression_statement = opt expression .> t ";"
grammer Compound_statement = t "{" .> opt declaration_list .> opt statement_list .> t "}"
grammer Statement_list =
    statement ./
    statement_list .> statement
grammer Selection_statement =
    t "if" .> t "(" .> expression .> t ")" .> statement ./
    t "if" .> t "(" .> expression .> t ")" .> statement .> t "else" .> statement ./
    t "switch" .> t "(" .> expression .> t ")" .> statement
grammer Iteration_statement =
    t "while" .> t "(" .> expression .> t ")" .> statement ./
    t "do" .> statement .> t "while" .> t "(" .> expression .> t ")" .> t ";" ./
    t "for" .> t "(" .> opt expression .> t ";" .> opt expression .> t ";" .> opt expression .> t ")" .> statement
grammer Jump_statement =
    t "goto" .> identifier .> t ";" ./
    t "continue" .> t ";" ./
    t "break" .> t ";" ./
    t "return" .> opt expression .> t ";"
grammer Expression =
    assignment_expression ./
    expression .> t "," .> assignment_expression
grammer Assignment_expression =
    conditional_expression ./
    unary_expression .> assignment_operator .> assignment_expression
grammer Assignment_operator =
    t "=" ./ t "*=" ./ t "/=" ./ t "%=" ./ t "+=" ./ t "-=" ./ t "<<=" ./ t ">>=" ./ t "&=" ./ t "^=" ./ t "|= "
grammer Conditional_expression =
    logical_OR_expression ./
    logical_OR_expression .> t "?" .> expression .> t ":" .> conditional_expression
grammer Constant_expression =
    conditional_expression
grammer Logical_OR_expression =
    logical_AND_expression ./
    logical_OR_expression .> t "||" .> logical_AND_expression
grammer Logical_AND_expression =
    inclusive_OR_expression ./
    logical_AND_expression .> t "&&" .> inclusive_OR_expression
grammer Inclusive_OR_expression =
    exclusive_OR_expression ./
    inclusive_OR_expression .> t "|" .> exclusive_OR_expression
grammer Exclusive_OR_expression =
    and_expression ./
    exclusive_OR_expression .> t "^" .> and_expression
grammer And_expression =
    equality_expression ./
    and_expression .> t "&" .> equality_expression
grammer Equality_expression =
    relational_expression ./
    equality_expression .> t "==" .> relational_expression ./
    equality_expression .> t "!=" .> relational_expression
grammer Relational_expression =
    shift_expression ./
    relational_expression .> t "<" .> shift_expression ./
    relational_expression .> t ">" .> shift_expression ./
    relational_expression .> t "<=" .> shift_expression ./
    relational_expression .> t ">=" .> shift_expression
grammer Shift_expression =
    additive_expression ./
    shift_expression .> t "<<" .> additive_expression ./
    shift_expression .> t ">>" .> additive_expression
grammer Additive_expression =
    multiplicative_expression ./
    additive_expression .> t "+" .> multiplicative_expression ./
    additive_expression .> t "-" .> multiplicative_expression
grammer Multiplicative_expression =
    cast_expression ./
    multiplicative_expression .> t "*" .> cast_expression ./
    multiplicative_expression .> t "/" .> cast_expression ./
    multiplicative_expression .> t "%" .> cast_expression
grammer Cast_expression =
    unary_expression ./
    t "(" .> type_name .> t ")" .> cast_expression
grammer Unary_expression =
    postfix_expression ./
    t "++" .> unary_expression ./
    t "--" .> unary_expression ./
    unary_expression .> cast_expression ./
    t "sizeof" .> unary_expression ./
    t "sizeof" .> t "(" .> type_name .> t ")"
grammer Unary_operator =
    t "&" ./ t "*" ./ t "+" ./ t "-" ./ t "~" ./ t "!"
grammer Postfix_expression =
    primary_expression ./
    postfix_expression .> t "[" .> expression .> t "]" ./
    postfix_expression .> t "(" .> opt argument_expression_list .> t ")" ./
    postfix_expression .> t "." .> identifier ./
    postfix_expression .> t "->" .> identifier ./
    postfix_expression .> t "++" ./
    postfix_expression .> t "--"
grammer Primary_expression =
    identifier ./
    constant ./
    string ./
    t "(" .> expression .> t ")"
grammer Argument_expression_list =
    assignment_expression ./
    argument_expression_list .> t "," .> assignment_expression    
grammer Constant =
    integer_constant ./
    character_constant ./
    floating_constant ./
    enumeration_constant

*Main> filter is_direct_left_recursion all_nt 
[Translation_unit,Declaration_list,Struct_declaration_list,Init_declarator_list,Struct_declarator_list,Enumerator_list,Direct_declarator,Type_qualifier_list,Parameter_list,Identifier_list,Initializer_list,Direct_abstract_declarator,Statement_list,Expression,Logical_OR_expression,Logical_AND_expression,Inclusive_OR_expression,Exclusive_OR_expression,And_expression,Equality_expression,Relational_expression,Shift_expression,Additive_expression,Multiplicative_expression,Unary_expression,Postfix_expression,Argument_expression_list]

*Main> filter is_mutually_left_recursion  all_nt 
[]

これそもそも正しく実装出来てるかどうか分かりませんけど、ちゃんと動いてるとすれば、一応直接左再帰除去を27の生成規則に適用すれば、再帰下降パーザでも取りあえずなんとか的な…。

Alloyで少しだけ遊ぶ

Alloyでゲームについて調べようの回！！

お題は、3x3の9マスでの○×ゲーム(三目並べ)は、先手必勝となるかどうか、です。

簡単なゲームから考える

まず次のような非常に簡単なゲームを考えます。

場にA , B , Cという3つの石がある。3種類じゃなくて、本当に3つしか石はない！
2人のプレーヤーで交互に場から石を取って自分のものにする。ただしパスはダメ。

先に"AとC"の両方を手に入れたものが勝利。

このゲーム、先手が有利なのは明らかです。取りあえず2つは石を取らないと勝ち目がないわけで、後手だと1つしか取れないわけです。

では先手がどれぐらい有利なのか。１つの指標として、「先手必勝」かどうかを考えます。

普通に考えれば、先手はAかCを取って、次に残りを取ろうとします。後手は、先手が次に取ろうとしているものを取れば、引き分けに成る筈です。
だから先手必勝ではない…。

ということで、本当に先手必勝でないかどうかをAlloyを使って調べてみましょう。
方針としては、先手必勝になるという命題を記述してそれが絶対に正しいかどうかをassertionで調べるというものです。ダメなら反例が出る筈です。

ここで重要なのは、どう書けばAlloyで楽に書けるか。皆さんも少し考えてみてください。

私は次のように書きました。

abstract sig Ishi { } // 石という集合を定義
one sig A , B , C extends Ishi {}  // ゲームで使う石はA , B , Cという3つに限る

assert sente_always_win {
	some X : Ishi | all Y : Ishi - X | some Z : Ishi - X - Y | X + Z in A + C
}

check sente_always_win

アサーション「先手必勝」は、先手は以下の制約を満たすXを取る事が出来る事を言っています。
制約 : 後手がXを除いたどんなYを取った場合でも、更に先手が残るたった１つのZについて、XとZは実はAとCの組になっている。

これが満たせるなら、先手必勝となる先手の石の取り方が確かに存在するという事になります。

ところが実際は、Xとしてどんなに上手くとっても、後手のYによって「邪魔」されてしまうのは前に述べた通りです。なので、この例だと反例が発生するはずです。実際に調べてみると…。

skolem $sente_always_win_Y={A$0->C$0, B$0->C$0, C$0->A$0}

という結果を得ます。それとなく見ると、何かに気付けると思います。

そう、これは実は、後手が先手の勝利を防ぐパターンになっているのです！！！

先手がAを取ったら、俺はCを取る！
先手がBを取ったら、俺はCを取る！
先手がCを取ったら、俺はAを取る！

戦略はもう1種類あります。

skolem $sente_always_win_Y={A$0->C$0, B$0->A$0, C$0->A$0}

これもAlloyが教えてくれます。

○×ゲームに戻る

では、○×ゲームはどうAlloyで記述すれば楽に書けるのでしょうか。まぁぼくは良く分からないので、先の考えを本当にそのまんま使って、次のように書きました。

abstract sig Board {
	right : lone Board ,
	up    : lone Board ,
	down : lone Board
}

one sig
A , B , C ,
D , E , F ,
G , H , I extends Board {}

fact {
	A.right = B B.right = C C.right = none
	D.right = E E.right = F F.right = none
	G.right = H H.right = I I.right = none

	A.down = D B.down = E C.down = F
	D.down = G E.down = H F.down = I
	G.down = none H.down = none I.down = none

	all X : Board | all Y : Board | X.down = Y <=> Y.up = X
}

pred win(have : set Board) {
	some p : have | 
	(
		(#p.^right = 2 && p.^right in have) ||
		(#p.^down = 2 && p.^down in have) ||
		(#p.^(right.down) = 2 && p.^(right.down) in have) ||
		(#p.^(right.up) = 2 && p.^(right.up) in have)
	)
}

assert always_win {
	some X_1 : Board                | let Xs = X_1 |
	all      Y_1 : Board - Xs        | let Ys = Y_1 |
	some X_2 : Board - Xs - Ys | let Xs = Xs + X_2 |
	all      Y_2 : Board - Xs - Ys | let Ys = Ys + Y_2 |
	some X_3 : Board - Xs - Ys | let Xs = Xs + X_3 | win[Xs] or (
	all      Y_3 : Board - Xs - Ys | let Ys = Ys + Y_3 | (not win[Ys]) && (
	some X_4 : Board - Xs - Ys | let Xs = Xs + X_4 | win[Xs] or (
	all      Y_4 : Board - Xs - Ys | let Ys = Ys + Y_4 | (not win[Ys]) && (
	some X_5 : Board - Xs - Ys | let Xs = Xs + X_5 | win[Xs] ) ) ) )
}

check always_win

かなり強引ですが、まぁ単純ではあります。ではこれを動かしてみましょう！！！先手必勝と言えるのか！！！

結果は

ダメ！！！ 反例が見つかりました。どんな感じかというと…

skolem $always_win_Y_1={A$0->E$0, B$0->H$0, C$0->E$0, D$0->F$0, E$0->I$0, F$0->E$0, G$0->E$0, H$0->E$0, I$0->E$0}

skolem $always_win_Y_2={A$0->B$0->C$0, A$0->C$0->B$0, A$0->D$0->G$0, A$0->F$0->C$0, A$0->G$0->D$0, A$0->H$0->D$0, A$0->I$0->B$0, B$0->A$0->C$0, B$0->C$0->A$0, B$0->D$0->A$0, B$0->E$0->A$0, B$0->F$0->A$0, B$0->G$0->A$0, B$0->I$0->A$0, C$0->A$0->B$0, C$0->B$0->A$0, C$0->D$0->G$0, C$0->F$0->I$0, C$0->G$0->B$0, C$0->H$0->I$0, C$0->I$0->F$0, D$0->A$0->G$0, D$0->B$0->A$0, D$0->C$0->G$0, D$0->E$0->G$0, D$0->G$0->A$0, D$0->H$0->G$0, D$0->I$0->G$0, E$0->A$0->C$0, E$0->B$0->H$0, E$0->C$0->G$0, E$0->D$0->F$0, E$0->F$0->D$0, E$0->G$0->C$0, E$0->H$0->B$0, F$0->A$0->C$0, F$0->B$0->A$0, F$0->C$0->I$0, F$0->D$0->B$0, F$0->G$0->I$0, F$0->H$0->I$0, F$0->I$0->C$0, G$0->A$0->D$0, G$0->B$0->D$0, G$0->C$0->B$0, G$0->D$0->A$0, G$0->F$0->C$0, G$0->H$0->I$0, G$0->I$0->H$0, H$0->A$0->F$0, H$0->B$0->G$0, H$0->C$0->I$0, H$0->D$0->I$0, H$0->F$0->I$0, H$0->G$0->I$0, H$0->I$0->G$0, I$0->A$0->H$0, I$0->B$0->C$0, I$0->C$0->F$0, I$0->D$0->B$0, I$0->F$0->C$0, I$0->G$0->H$0, I$0->H$0->G$0}

skolem $always_win_Y_3={A$0->B$0->D$0->G$0, A$0->B$0->F$0->G$0, A$0->B$0->G$0->D$0, A$0->B$0->H$0->I$0, A$0->B$0->I$0->H$0, A$0->C$0->D$0->H$0, A$0->C$0->F$0->I$0, A$0->C$0->G$0->H$0, A$0->C$0->H$0->G$0, A$0->C$0->I$0->H$0, A$0->D$0->B$0->C$0, A$0->D$0->C$0->B$0, A$0->D$0->F$0->C$0, A$0->D$0->H$0->I$0, A$0->D$0->I$0->H$0, A$0->F$0->B$0->I$0, A$0->F$0->D$0->G$0, A$0->F$0->G$0->D$0, A$0->F$0->H$0->I$0, A$0->F$0->I$0->G$0, A$0->G$0->B$0->F$0, A$0->G$0->C$0->B$0, A$0->G$0->F$0->I$0, A$0->G$0->H$0->I$0, A$0->G$0->I$0->H$0, A$0->H$0->B$0->F$0, A$0->H$0->C$0->F$0, A$0->H$0->F$0->I$0, A$0->H$0->G$0->I$0, A$0->H$0->I$0->G$0, A$0->I$0->C$0->H$0, A$0->I$0->D$0->G$0, A$0->I$0->F$0->H$0, A$0->I$0->G$0->H$0, A$0->I$0->H$0->G$0, B$0->A$0->D$0->G$0, B$0->A$0->E$0->I$0, B$0->A$0->F$0->I$0, B$0->A$0->G$0->D$0, B$0->A$0->I$0->E$0, B$0->C$0->D$0->F$0, B$0->C$0->E$0->G$0, B$0->C$0->F$0->I$0, B$0->C$0->G$0->E$0, B$0->C$0->I$0->F$0, B$0->D$0->C$0->I$0, B$0->D$0->E$0->F$0, B$0->D$0->F$0->E$0, B$0->D$0->G$0->F$0, B$0->D$0->I$0->F$0, B$0->E$0->C$0->G$0, B$0->E$0->D$0->F$0, B$0->E$0->F$0->D$0, B$0->E$0->G$0->C$0, B$0->E$0->I$0->F$0, B$0->F$0->C$0->I$0, B$0->F$0->D$0->E$0, B$0->F$0->E$0->D$0, B$0->F$0->G$0->E$0, B$0->F$0->I$0->C$0, B$0->G$0->C$0->E$0, B$0->G$0->D$0->E$0, B$0->G$0->E$0->C$0, B$0->G$0->F$0->E$0, B$0->G$0->I$0->E$0, B$0->I$0->C$0->F$0, B$0->I$0->D$0->E$0, B$0->I$0->E$0->F$0, B$0->I$0->F$0->C$0, B$0->I$0->G$0->F$0, C$0->A$0->D$0->H$0, C$0->A$0->F$0->I$0, C$0->A$0->G$0->D$0, C$0->A$0->H$0->I$0, C$0->A$0->I$0->H$0, C$0->B$0->D$0->I$0, C$0->B$0->F$0->I$0, C$0->B$0->G$0->I$0, C$0->B$0->H$0->I$0, C$0->B$0->I$0->F$0, C$0->D$0->A$0->B$0, C$0->D$0->B$0->A$0, C$0->D$0->F$0->I$0, C$0->D$0->H$0->I$0, C$0->D$0->I$0->F$0, C$0->F$0->A$0->B$0, C$0->F$0->B$0->A$0, C$0->F$0->D$0->H$0, C$0->F$0->G$0->H$0, C$0->F$0->H$0->G$0, C$0->G$0->A$0->H$0, C$0->G$0->D$0->H$0, C$0->G$0->F$0->I$0, C$0->G$0->H$0->I$0, C$0->G$0->I$0->H$0, C$0->H$0->A$0->B$0, C$0->H$0->B$0->A$0, C$0->H$0->D$0->G$0, C$0->H$0->F$0->G$0, C$0->H$0->G$0->B$0, C$0->I$0->A$0->D$0, C$0->I$0->B$0->D$0, C$0->I$0->D$0->G$0, C$0->I$0->G$0->H$0, C$0->I$0->H$0->G$0, D$0->A$0->B$0->C$0, D$0->A$0->C$0->B$0, D$0->A$0->E$0->I$0, D$0->A$0->H$0->I$0, D$0->A$0->I$0->E$0, D$0->B$0->C$0->E$0, D$0->B$0->E$0->H$0, D$0->B$0->G$0->H$0, D$0->B$0->H$0->E$0, D$0->B$0->I$0->H$0, D$0->C$0->A$0->B$0, D$0->C$0->B$0->A$0, D$0->C$0->E$0->I$0, D$0->C$0->H$0->B$0, D$0->C$0->I$0->A$0, D$0->E$0->A$0->I$0, D$0->E$0->B$0->H$0, D$0->E$0->C$0->A$0, D$0->E$0->H$0->B$0, D$0->E$0->I$0->A$0, D$0->G$0->B$0->I$0, D$0->G$0->C$0->E$0, D$0->G$0->E$0->C$0, D$0->G$0->H$0->I$0, D$0->G$0->I$0->H$0, D$0->H$0->A$0->I$0, D$0->H$0->B$0->E$0, D$0->H$0->C$0->B$0, D$0->H$0->E$0->B$0, D$0->H$0->I$0->E$0, D$0->I$0->A$0->E$0, D$0->I$0->B$0->E$0, D$0->I$0->C$0->E$0, D$0->I$0->E$0->A$0, D$0->I$0->H$0->A$0, E$0->A$0->B$0->H$0, E$0->A$0->D$0->F$0, E$0->A$0->F$0->D$0, E$0->A$0->G$0->D$0, E$0->A$0->H$0->F$0, E$0->B$0->A$0->G$0, E$0->B$0->C$0->G$0, E$0->B$0->D$0->G$0, E$0->B$0->F$0->D$0, E$0->B$0->G$0->C$0, E$0->C$0->A$0->B$0, E$0->C$0->B$0->H$0, E$0->C$0->D$0->H$0, E$0->C$0->F$0->H$0, E$0->C$0->H$0->B$0, E$0->D$0->A$0->C$0, E$0->D$0->B$0->C$0, E$0->D$0->C$0->G$0, E$0->D$0->G$0->C$0, E$0->D$0->H$0->B$0, E$0->F$0->A$0->G$0, E$0->F$0->B$0->H$0, E$0->F$0->C$0->G$0, E$0->F$0->G$0->C$0, E$0->F$0->H$0->B$0, E$0->G$0->A$0->D$0, E$0->G$0->B$0->H$0, E$0->G$0->D$0->F$0, E$0->G$0->F$0->D$0, E$0->G$0->H$0->B$0, E$0->H$0->A$0->G$0, E$0->H$0->C$0->G$0, E$0->H$0->D$0->F$0, E$0->H$0->F$0->D$0, E$0->H$0->G$0->C$0, F$0->A$0->B$0->I$0, F$0->A$0->D$0->G$0, F$0->A$0->G$0->D$0, F$0->A$0->H$0->I$0, F$0->A$0->I$0->G$0, F$0->B$0->C$0->I$0, F$0->B$0->D$0->H$0, F$0->B$0->G$0->H$0, F$0->B$0->H$0->I$0, F$0->B$0->I$0->C$0, F$0->C$0->A$0->B$0, F$0->C$0->B$0->A$0, F$0->C$0->D$0->H$0, F$0->C$0->G$0->H$0, F$0->C$0->H$0->D$0, F$0->D$0->A$0->G$0, F$0->D$0->C$0->I$0, F$0->D$0->G$0->A$0, F$0->D$0->H$0->I$0, F$0->D$0->I$0->C$0, F$0->G$0->A$0->D$0, F$0->G$0->B$0->D$0, F$0->G$0->C$0->D$0, F$0->G$0->D$0->A$0, F$0->G$0->H$0->D$0, F$0->H$0->A$0->G$0, F$0->H$0->B$0->G$0, F$0->H$0->C$0->G$0, F$0->H$0->D$0->G$0, F$0->H$0->G$0->D$0, F$0->I$0->A$0->H$0, F$0->I$0->B$0->H$0, F$0->I$0->D$0->G$0, F$0->I$0->G$0->H$0, F$0->I$0->H$0->G$0, G$0->A$0->B$0->F$0, G$0->A$0->C$0->F$0, G$0->A$0->F$0->I$0, G$0->A$0->H$0->I$0, G$0->A$0->I$0->F$0, G$0->B$0->A$0->C$0, G$0->B$0->C$0->A$0, G$0->B$0->F$0->I$0, G$0->B$0->H$0->I$0, G$0->B$0->I$0->H$0, G$0->C$0->A$0->D$0, G$0->C$0->D$0->A$0, G$0->C$0->F$0->I$0, G$0->C$0->H$0->I$0, G$0->C$0->I$0->H$0, G$0->D$0->B$0->I$0, G$0->D$0->C$0->I$0, G$0->D$0->F$0->I$0, G$0->D$0->H$0->I$0, G$0->D$0->I$0->H$0, G$0->F$0->A$0->D$0, G$0->F$0->B$0->I$0, G$0->F$0->D$0->A$0, G$0->F$0->H$0->I$0, G$0->F$0->I$0->H$0, G$0->H$0->A$0->D$0, G$0->H$0->B$0->C$0, G$0->H$0->C$0->D$0, G$0->H$0->D$0->A$0, G$0->H$0->F$0->C$0, G$0->I$0->A$0->D$0, G$0->I$0->B$0->F$0, G$0->I$0->C$0->F$0, G$0->I$0->D$0->B$0, G$0->I$0->F$0->C$0, H$0->A$0->B$0->D$0, H$0->A$0->C$0->D$0, H$0->A$0->D$0->G$0, H$0->A$0->G$0->D$0, H$0->A$0->I$0->G$0, H$0->B$0->A$0->C$0, H$0->B$0->C$0->A$0, H$0->B$0->D$0->I$0, H$0->B$0->F$0->I$0, H$0->B$0->I$0->D$0, H$0->C$0->A$0->B$0, H$0->C$0->B$0->A$0, H$0->C$0->D$0->G$0, H$0->C$0->F$0->B$0, H$0->C$0->G$0->F$0, H$0->D$0->A$0->G$0, H$0->D$0->B$0->G$0, H$0->D$0->C$0->G$0, H$0->D$0->F$0->G$0, H$0->D$0->G$0->A$0, H$0->F$0->A$0->D$0, H$0->F$0->B$0->G$0, H$0->F$0->C$0->G$0, H$0->F$0->D$0->G$0, H$0->F$0->G$0->B$0, H$0->G$0->A$0->D$0, H$0->G$0->B$0->F$0, H$0->G$0->C$0->F$0, H$0->G$0->D$0->A$0, H$0->G$0->F$0->D$0, H$0->I$0->A$0->D$0, H$0->I$0->B$0->F$0, H$0->I$0->C$0->F$0, H$0->I$0->D$0->F$0, H$0->I$0->F$0->C$0, I$0->A$0->B$0->C$0, I$0->A$0->C$0->B$0, I$0->A$0->D$0->G$0, I$0->A$0->F$0->C$0, I$0->A$0->G$0->D$0, I$0->B$0->A$0->H$0, I$0->B$0->D$0->H$0, I$0->B$0->F$0->H$0, I$0->B$0->G$0->H$0, I$0->B$0->H$0->G$0, I$0->C$0->A$0->B$0, I$0->C$0->B$0->D$0, I$0->C$0->D$0->H$0, I$0->C$0->G$0->D$0, I$0->C$0->H$0->G$0, I$0->D$0->A$0->H$0, I$0->D$0->C$0->F$0, I$0->D$0->F$0->H$0, I$0->D$0->G$0->H$0, I$0->D$0->H$0->G$0, I$0->F$0->A$0->G$0, I$0->F$0->B$0->H$0, I$0->F$0->D$0->G$0, I$0->F$0->G$0->H$0, I$0->F$0->H$0->G$0, I$0->G$0->A$0->D$0, I$0->G$0->B$0->F$0, I$0->G$0->C$0->B$0, I$0->G$0->D$0->B$0, I$0->G$0->F$0->C$0, I$0->H$0->A$0->F$0, I$0->H$0->B$0->F$0, I$0->H$0->C$0->F$0, I$0->H$0->D$0->F$0, I$0->H$0->F$0->C$0}

これを使えば、3x3の○×ゲームでは負けることは無いですね！！

このお話で何が言いたかったか

実はこの3x3の○×ゲームで先手必勝がない事を言うのに3,4時間はかけました…。

というのは、どうやればAlloyで簡単に書けるか考えたり(面倒臭い書き方は嫌ですし)、sequenceという列を作ってあれこれするモジュールがあるので、それ使って石の選び方の列のようなものを作って…などなど考えたり、実際に書いたり、色々嵌って困るという事を一通りしました。

で、上のsomeとallが交互に出現するパターンはどこから出したかというと、ゲームの手番のやりとりをどう実装するかということではなくて、そもそもの「何が言えれば先手必勝が言えるか」を考え直してみたという所です。

そうするとあとに残るのは、縦横ナナメに揃っているかどうかを調べる述語を追加してあげれば良いだけです。これについても、Alloyに組込まれている「関係の推移閉包を求める」機能を使いました。まぁ細かい事は、「抽象によるソフトウェア設計を参考にしてください！」という事で。

また、Alloyはどのようにしてこの反例を見付けたのかという事についての興味が出た方もいると思います。
重要なのは、出力結果の中にも出て来ているのですがskolem化というものです。
スコーレム化そのものは、述語論理のエルブランの定理などの文脈などで自然(…?)に出てくるのですがまぁ詳しくは適当なLogicの本も参考にしてください。

それで結局なんなのかというと、ぼくは出来るだけAlloyっぽく手抜きして気楽に書こうという事だけをひたすら考えて上のものを作ったのですが、他の人が挑戦するとどんな感じに短くなるのかなーという所に興味があるので、
皆さんも簡単な練習問題としてやってみてくださいよーということでした。

いやーでも慣れて無いというのは勿論あるのですが、ただでさえこう動き辛い感じなので少しでも余計な事しようとするとすぐにこれは無理だやめようみたいな感じになるのは果たしてどう効いてくるのかっていうのが。

まぁでも上から被せて機械に頑張らせるっていうのは21世紀は人間の時代なので間違って無いと信じています。

「抽象によるソフトウェア設計」発売

https://sites.google.com/site/softwareabstractionsja/
https://sites.google.com/site/softwareabstractionsja/about/toc ← 目次

本日7月15日金曜日、洋書「Software Abstractions」(http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928)の訳本である「抽象によるソフトウェア設計 Alloyではじめる形式手法」が発売されます。

実はレビュワーだったりしたので、発売当日になってしまいましたが、勝手に紹介するつもりです。

さて、本書はサブタイトルの通りでAlloyを使って何か色々しましょうという感じになっています。

いや、そもそも"Alloy"って何やねんという話なのですが、Alloy 知らなくても読めるという感じのするサブタイトルですね！！
(ちなみにAlloyの最新バージョンであるAlloy4は次のサイトから入手出来ます → http://alloy.mit.edu/alloy4/)

中身の紹介に入る前ですが、皆さん、「抽象」「設計」「はじめる〜」「形式手法」などの文字列が目に入り込んで来た瞬間に「はぁまたこのような本が出たとは！」「読んでも何も変わるまい」「まぁわたくしには関係ありませんわね(迫真)」などなど考えた筈です。

宣伝にあたってこう書くとなんですが、本書は「はじめる形式手法」とかゆるふわっぽいタイトルになっているものの、実はそんなに簡単な内容ではないという所が味噌です。かなり骨のある書だと思います。

うだうだ言っても何なので、そもそもAlloyで何が出来るのか。

そんな上手く短く書けないので、インターネット上に存在するAlloyの良いtutorialへのリンクを貼ってみます。
http://people.csail.mit.edu/eskang/talks/alloy-tutorial-abz2010.pdf

Alloyは非常に簡単に言うと「関係論理」という論理の1種を用いて、調べたい対象を記述、それと同時に対象において成立するべき/成立してはならない事柄を書いて、それが正しくそうなっているかどうかを調べるというものです。
「正しくそうなっている」かどうか、どうやって確認するのか? というのは、何それの事柄を満たす「モデル、インスタンス、具体例」を発見出来るか、発見出来ないかによって調べるのです。
モデルを発見しようとするのがAlloyの仕事です。あることを証明したり、ないことを証明したりするわけではありません。

関係論理って何やねんという話ですが、関係(relation)を要とする論理系の一種とかその程度の理解で十分です。

さて、このAlloyを使ってどのような対象にあれやこれやを記述する事が出来るのでしょうか?
例えば、上述のtutorialの最初の方では「アドレス帳」を書いています。

sig Name , Addr {}

sig Book {
  addr : Name -> lone Addr
// お手軽にloneて何なのか知りたい そこのあなたは、是非本で確認してください
}

Nameというモノ(名前を意図しています)の集まり、Addrというモノ(アドレスを意図しています)の集まりを1行目で定義しているのです。
3行目からは、Bookというモノ(意味的にはアドレス帳)と、addrという「関係」を定義しています。

この関数っぽく見える関係addrですが、(アドレス帳 , 名前 , アドレス)の3つ組に関する関係になっています。

このような関係を定義して、その上で色々やるというのがAlloy上で行う事になるのですが、果たしてどんなものなら記述出来るのでしょうか?

例えば、固定したアドレス帳のある瞬間における静的な状態として、1つの名前に対して登録出来るアドレスは「高々1件である」という制約(上述のAlloyコードはそういう事を述べている)は記述出来るわけですが、では動的な操作に対してはどのようにすれば良いでしょう。

えーと…アドレス帳上では追加や削除といった操作を行ったりします。
ここで追加や削除は実装されているとして、実装はさておきで追加や削除が「満たすべき」振舞というものは存在します。

アドレス帳に存在しない名前に対してアドレスを登録した(追加)。
そしてその直後にその名前を消した(削除)ならば、元のアドレス帳と同じになっていなければならない。

そのような追加と削除に関する簡単な仕様は記述出来ます。

この手の「シミュレーション」ぽい事をどう行うのかというのはイディオムとしても、設計を行う上でも大変重要なものです。先のtutorialではざっくり様々な方法を書いていますが、詳しくは本書を手に入れてくださいという事で…。

Alloy何が面白いの?

何ソレが出来るみたいなポジショントーク的なものはさておき、Alloyを使っていて面白いのは自分が直面している問題をどうAlloyで取り組める/取り組み易い形にエンコードするかという事です。

Alloyは実際書いてみると分かりますが、(ほぼ)1階述語論理を使って様々なものを捉え直す必要が出てくるわけで、状態を激しく持ち回すようなものや、実際に実装しなければならないフルセットでエンコードするとか、そういったものは上手くいかないだとか、面倒臭いという事が多いものです。

結果的に取捨選択のもとでエンコードする事が多く成るわけですが、それは問題を抽象化してシンプルにするという事だけでは足りず、問題の捉え直しが必要だったり、一般化が必要になったりします。

ある種の縛りプレイのようなものだと思うのですが、それによって結果的に見通しや理解が深まる事というのは意外にも多いです。というより単純に楽しいです。

そして、このような論理を用いた「あれこれ」の記述に、慣れる事が出来るというのも大切なことだと思います。
巷では定理証明支援系が云々というのがありますが、何にせよ「自分の言いたい事をどう形式的に記述するか」という能力は問われるものです。そのような能力を養う事も出来ると思います。

この「Alloyでどう書く?」的な具体例の1つとして、tutorialの最後の方で出てくる「Checking Data Refinement」が面白いと思います。

最後に

最後に成りますが、本書は豊富な例と、的を得たFAQを兼ね備えており、あれこれ考えながら読む事が出来る構成になっていると思います。

昨今は様々な「プログラミング言語」が盛衰していますが、ここでちょっと毛色の違う「Alloy言語」はどうでしょうか！！

今までの経験をAlloyを使う時にも活かせますし、新たに学んだ事を、例え実際にAlloyを使わなくてもコードの中で活かす事が出来ると思います。是非夏休みの一冊に。

スタートClean

7月9日の13時から株式会社SpeeeさんでCleanランゲッジのイントロダクションの話があるらしいです。

後11人ぐらい参加出来るようなので、自称CleanプロからCleanの開発者の皆様、最底辺プログラマであるボクにモノを是非教えてくださいませ。

http://partake.in/events/efad035a-0dbe-4717-aa5d-1afb320e05d6

主催者のoskimuraさんに多謝。

彼女の友人がGCCの中の人から聞いた話

以下，エイプリルフールの記事として書いたものなので現代において読む価値はありません．

ブログには地震後初めて記事を書く事になって、生存報告としては明らかに遅いですね…。でも、twitterでは元気にやっていました。今は実家にいます。

さて、つい先日東京で言語雑談会というイベントがあって、その折につくばのお家の現状を見て来ました。特別大変な事が起こっていたわけでもなく心底ホッとしました。
その翌日には、彼女と東京は新宿バルト9でサヨナラノツバサを観たのですが、その折にgcc-4.6( http://gcc.gnu.org/gcc-4.6/changes.html )の話がでました。

gccの話が出たのはCランゲッジの話をしていたからなのですが、sequence pointをどうして副作用完了点と訳したのでしょうか、とかそういう疑問が発端だった気がします。
"副作用完了点"を認識した事の無い方は、次の参考ページを一読すると大変良いと思います。改めて考えると、ぼくはそんなに意識していませんでしたが…。 → http://www.jpcert.or.jp/sc-rules/c-exp30-c.html

さて、その時の話の核心というのは、gcc-4.6におけるundocumentedな最適化の話です。
次のようなコードを見てください。

#include <stdio.h>
#include <stdint.h>
#include <assert.h>
#include <stdlib.h>

uint64_t fib(uint64_t x)
{
    assert(1 <= x);
    if(x == 1)return 1;
    else if(x == 2)return 1;
    else return fib(x-1) + fib(x-2);
}

void print(uint64_t v0,uint64_t v1,uint64_t v2)
{
    printf("v0 = %llu\n",v0);
    printf("v1 = %llu\n",v1);
    printf("v2 = %llu\n",v2);
}

int main()
{
    print(fib(38),fib(39),fib(40));

    return 0;
}

取りあえずこれを実行してみます。

/Users/ranha/Blog/2011AprilFool% gcc -Wall nyan.c -o a.out
/Users/ranha/Blog/2011AprilFool% time ./a.out
v0 = 39088169
v1 = 63245986
v2 = 102334155
./a.out  3.94s user 0.01s system 99% cpu 3.977 total

フムフム。
そして、ここでその友人から教わったというオプションを付けてみます。

nazo-option
zikkou

フムフム！こちらの方が明らかに速いですね！！

しかし何をしているのだろう…

良く分からないので、gdbを使って調べてみました…。要所要所を抜き出すと…

Breakpoint 1, main () at nyan.c:
23	{
(gdb) n
22	int main()
(gdb) 
38	    if(pthread_create(&thread_a,NULL,a,NULL))exit(1);
(gdb) 
[New Thread 0xaacb70 (LWP 4493)]
39	    if(pthread_create(&thread_b,NULL,b,NULL))exit(1);
(gdb) 
[New Thread 0x12adb70 (LWP 4494)]
40	    if(pthread_create(&thread_c,NULL,c,NULL))exit(1);
(gdb) 
[New Thread 0x1aaeb70 (LWP 4495)]
41	    pthread_join(thread_a,&dummy[0]);
(gdb) 
[Thread 0xaacb70 (LWP 4493) exited]
42	    pthread_join(thread_b,&dummy[1]);
(gdb) 
[Thread 0x12adb70 (LWP 4494) exited]
43	    pthread_join(thread_c,&dummy[2]);
(gdb) 
[Thread 0x1aaeb70 (LWP 4495) exited]
44	    print(v0,v1,v2);
(gdb) 
v0 = 39088169
v1 = 63245986
v2 = 102334155
46	    return 0;

何だコレは！！！！！！

取りあえずシステム情報

/Users/ranha/Blog/2011AprilFool% uname -a
Darwin ranha-macbook.local 10.6.0 Darwin Kernel Version 10.6.0 とか
/Users/ranha/Blog/2011AprilFool% gcc --version
gcc (GCC) 4.6.0 20110401 (experimental)
Copyright (C) 2011 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

こんなコードを生成するらしい

上のフィボナッチ数を計算するコードから、次のようなコードを生成するようです。

#include <stdio.h>
#include <stdint.h>
#include <assert.h>
#include <stdlib.h>
#include <pthread.h>

uint64_t fib(uint64_t x)
{
    assert(1 <= x);
    if(x == 1)return 1;
    else if(x == 2)return 1;
    else return fib(x-1) + fib(x-2);
}

void print(uint64_t v0,uint64_t v1,uint64_t v2)
{
    printf("v0 = %llu\n",v0);
    printf("v1 = %llu\n",v1);
    printf("v2 = %llu\n",v2);
}

int main()
{
    uint64_t v0,v1,v2;
    pthread_t thread_a;
    pthread_t thread_b;
    pthread_t thread_c;
    void *dummy[3];
    void* a(void* _){
        v0 = fib(38);return NULL;
    }
    void* b(void* _){
        v1 = fib(39);return NULL;
    }
    void* c(void* _){
        v2 = fib(40);return NULL;
    }
    if(pthread_create(&thread_a,NULL,a,NULL))exit(1);
    if(pthread_create(&thread_b,NULL,b,NULL))exit(1);
    if(pthread_create(&thread_c,NULL,c,NULL))exit(1);
    pthread_join(thread_a,&dummy[0]);
    pthread_join(thread_b,&dummy[1]);
    pthread_join(thread_c,&dummy[2]);
    print(v0,v1,v2);

    return 0;
}

成る程、gccのnested function( http://gcc.gnu.org/onlinedocs/gcc/Nested-Functions.html )を使った実装で、カジュアルにpthreadに突っ込めるようにしている所が味噌なんですね。しかもnested functionにする事で、割と簡単にスコープのアレコレを解決出来るようになっていると！
(pthreadの扱いが凄い適当なのは御免なさいって事らしいです。)

でも引数の評価を並列にしてしまって問題無いのでしょうか??

これはつまり

f(e1,e2,...,en);

e1からenを並列に計算してもCランゲッジとして、問題は無いのか?という事です。

Cランゲッジは、その言語仕様として、関数の引数の評価に特定の順番を設けていません。
http://www.jpcert.or.jp/sc-rules/c-exp10-c.html

簡単な例を示します。

/* simple1.c */
#include <stdio.h>

int f(void){return puts("f");}
int g(void){return puts("g");}
void h(int a,int b){printf("a = %d,b = %d\n",a,b);}

int main(){
    h(f(),g());
    return 0;
}

/Users/ranha/Blog/2011AprilFool% gcc -Wall simple1.c && ./a.out
g                                                              
f                                                              
a = 10,b = 10                                                  
/Users/ranha/Blog/2011AprilFool% clang -Wall simple1.c && ./a.out
f                                                                
g                                                                
a = 10,b = 10

成る程、上の例でe1からenでお互いに「依存が存在しない場合」は、並列に動かしたとしても問題は無い気がします。

依存が存在する場合はどうか?

次のプログラムを考えてみます

#include <stdio.h>

int i = 0;

int f(void)
{
  return ++i;
}

int main()
{
  printf("%d %d\n",f(),f());
  return 0;
}

これを並列に実行した場合には、変数iに関して所謂data raceが発生してしまう気がします。所が、Cランゲッジの挙動としては、data raceが発生しても良いのです。

http://www.jpcert.or.jp/sc-rules/c-exp30-c.html

直前の副作用完了点から次の副作用完了点までの間に、式の評価によって1つのオブジェクトに格納された値を変更する回数は、高々1回でなければならない。さらに、変更前の値の読み取りは、格納される値を決定するためだけに行われなければならない。

引数の間に、副作用完了点が存在しないので、つまり上の例だと副作用完了点の間で、大域的な変数iに対して変更が「2回」行われている事に成ります。この場合は、挙動として"undefined"という事に成っています。

http://www.st.rim.or.jp/~phinloda/cqa/cqa7.html
未定義、即ち「鼻から悪魔が飛び出しても仕様に反しない」( http://groups.google.com/group/comp.std.c/msg/dfe1ef367547684b )わけです。

という事は、まぁ並列に走らせても問題はないのでしょう。

いや、嘘かもしれません。undefinedでは無い気がします。
printf中の2つのfのどちらを先に呼び出すのかという点では自由です。しかし、結局の所どちらかを先に呼び出さなければ成りません。
ここで、

int i=0;

int main()
{
  printf("%d %d\n",(λx . i+=1;i)(),(λx . i+=1;i)());
  return 0;
}

なものを考えた時に、副作用完了点の区間としては異なるうちでそれぞれiをmodifyしている気がするので…。

アイエエエ！ C99では、expression-statementというまぁ"exp;"の形の文の終了点に副作用完了点を持っているので、undefinedに成る事を利用した並列化は出来ない気がします。ムネン。

参考 : http://www.open-std.org/JTC1/SC22/wg14/www/docs/n1124.pdf (特にAnnex C)

本当にそう?

共通に可視な変数に対して、引数を評価している間(副作用完了点の間)に0回modify , 2回以上modifyの場合を考えました。では1回の場合で何か不味そうな事は起こるでしょうか?

#include <stdio.h>

int i = 0;

int f(void){ return i; }
int g(void){ i = 42; return i; }
int h(int a,int b){ ... }

int main()
{
  h(f(),g());
  return 0;
}

この場合にfとgが並列に実行されると…。これは高々1回に収まっているのでundefined behaviorでは有りませんが、並列実行した場合は良く無い事が起こる筈です。

この良く無い事は、「評価順に関してspecifyしない」というCランゲッジの仕様から導けない結果です。"順に1つずつ実行した場合"には"発生しえない"挙動をする可能性があります。

結果として

f(e1,e2,...,en);

の形でe1からenを並列に実行する事は単純には行えない事が分かりました。ので、残念ながら上のような最適化手法は使えそうにないです…。

他には何が出来る?

いなばさんの上記エントリに端を発した、「カジュアルのんでたーみにずむ」な話も言えたりします。

unspecifiedであるという事は、その解釈に余地が残されているわけで、私達は良く「処理系や環境依存ではないコードを書きましょう！」など言われるわけで、それ自体は良いのですが、そこからひいては「unspecifiedはどうしようも無い子だし、undefinedって何の為に生きているのでしょうか…」といった考え方になってしまいます。

ちょっと待った！！unspecifiedであるということ、undefinedであるという事をもっと利用出来ないか！！というのが本エントリを書くキッカケでした。

言語仕様におけるundefinedとunspecifiedについて、最近だとこんな話が。

テストに関するお話

TLDI2011でacceptedな話として http://blog.regehr.org/archives/492 があります。これは、differential testingという手法でCのコンパイラをテストしようぜ！！というものです。

differential testingというのは、仕様に関して妥当なプログラムを複数のコンパイラに突っ込んで、その振舞を調べる。振舞が違っていれば、コンパイラのどれかにバグがあるから、それを手がかりにして調べようというお話です。振舞が同じで、実は全てのコンパイラにバグがあるという事も起こりうる筈ですが、まぁそれは…ね。みたいな感じデス。詳しくは上記ブログから論文を読んでみてください。

ここで重要なのは、コンパイラ達の入力とするプログラムが「一意」になるという事です。
もう少し具体的に言うならば、「１つのプログラムから導かれる挙動がただ１つに定まる」という事です。
挙動と言っても、実行するタイミングでシステムコールの結果としての値が違ったりとかそういう細かい部分はあるのですが、それ以前の話として、「仕様レベルで」undefinedやunspecifiedに陥ってしまうコードを生成しないようにしよう、というものです。

そうすれば、一意に成る筈なのに違ってる → コンパイラが何か不味い！と言えそうです。

証明に関するお話

CompCertという検証されたコンパイラがあります。
http://compcert.inria.fr/
特に分かり易い論文は
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

CompCertは、ソース言語(Cの"サブセット")の意味が、コンパイルされた後のターゲット言語(PowerPCアセンブリ)でも保存されている事を証明した、しかも普通に使える程度に速いコンパイラです。

ここでCの"サブセット"(Clightと呼ばれています)を用いるのには、Cの振舞が「非決定」である所に起因しています。結果から言って、PowerPCアセンブリは「決定的」、つまり1つのコードから生まれる振舞は1つですが、大元のCのコードから生まれる振舞は1つでないわけです。

それだと「ソース言語プログラムの意味がターゲット言語に落ちた時に保存されている」事を証明するのが困難になってしまうので、そこで新たに、Cの仕様として解釈の余地が在った部分を詰め、決定的になったClightをソース言語とし形式化を行ったという話です。

裏を返せば

Cランゲッジは並列に評価出来る所はガンガンしちゃっても良いし、そもそも非決定！
しかも関数引数の評価順だけでなくて、他にもunspecifiedはあるのです。上述のCsmithの論文によると、C99のunspecifiedはその数52種

「好きなように解釈して、好きなようにコンパイラを作ろう！！」

Cランゲッジはまだまだはじまったばかり！！

おわりに

ぼくが欲しいのは、健全かつ完全にundefinedとunspecifiedを検出する多項式時間実行可能なツールですけどね…

guile-2.0がリリースされたので入れるだけ入れてみた

http://www.gnu.org/software/guile/news.html
去る2月16日に、GNUのGuile version 2.0がリリースされたのでそれのインストールメモというだけです。

http://lwn.net/Articles/428288/

近いうちに、Guile 2.0 Crashやりたいですね。近いうちっていうか本当は今月が良かったのですが今月ってあと一週間そこいらですし来週は色々イベントあるのと仕事で無理ですね。

FFIというよりもCとの双方向の色々がやり易いらしくて、そうすると色々実装どうなってるのかなーというのはかなり気になる所です。

環境

Darwin ranha-macbook.local 10.6.0 Darwin Kernel Version 10.6.0のi386とかそんなんです

gitから引っ張ってくる

http://www.gnu.org/software/guile/download.html#git
えっいきなり ftp://ftp.gnu.org/pub/gnu/guile/ じゃなくてgitリポジトリから取ってくるんですか?というのは、まぁ色々あったからですというか、gitリポジトリから取って来たヤツだと動いたって言うそれだけです。
普通にcloneすれば良いと思います。

autoreconf

gitから取って来たものにはconfigure入っていませんから、

autoreconf -i --verbose

などやって色々生成します。

AM_GNU_GETTEXTが無い、でもgettext-develとかは入れてるという場合は、aclocal --print-ac-dirなど見て、ちゃんとgettext.m4とか見付けられるか調べてあげてください。

configure

今回は特にくくらずに、

configure

とします。configureで失敗する場合は、C_INCLUDE_PATHとかで必要なものちゃんと見付けられているかっていういつものお話です。
それかconfigureデバッグをして切り抜けるかです。

makeすると失敗する

すくなくとも私の環境では、libguile.dylibとかそういうのを生成するタイミングで失敗します。エラー内容は多分

  1. rpl_putenvがundefined
  2. _environがundefined

とかそんな感じになると思います。

rpl_putenvについて

結論から言うと、C_INCLUDE_PATHで/usr/local/includeとか/usr/includeに通してる場合そっちを見に行ってしまうので困るよねとかそんなです多分。
まず１つ目のrpl_putenvですが、これはlib/stdlib.hを見ると740行あたりに

#if 1
# if 1
#  if !(defined __cplusplus && defined GNULIB_NAMESPACE)
#   undef putenv
#   define putenv rpl_putenv
#  endif
_GL_FUNCDECL_RPL (putenv, int, (char *string) _GL_ARG_NONNULL ((1)));
_GL_CXXALIAS_RPL (putenv, int, (char *string));
# else
_GL_CXXALIAS_SYS (putenv, int, (char *string));
# endif
_GL_CXXALIASWARN (putenv);
#endif

と書いています。libguile以下ではgcc -I../libなどしているので、libguileでのstdlib includeはlib/stdlib.hを指す事になります。で、configureで何もしなかったので_cplusplusがdefinedではないですから、putenvがrpl_putenvとなってしまうわけです。

いや、でもlib/putenv.cがあってそこで多分上手く動くだろうから大丈夫なのでは?というのは実は残念なことになってしまっていて…例えば次のCプログラム

/* test.c */
#include <stdlib.h> /* stdlib.hはカレントディレクトリに存在するとする */
int main()
{
    return 0;
}

%gcc -E test.c -I. | grep stdlib.h <- gcc -I$(pwd)などとしても意味ない
# 1 "/usr/include/stdlib.h" 1 3
# 61 "/usr/include/stdlib.h" 3
# 62 "/usr/include/stdlib.h" 2 3
# 64 "/usr/include/stdlib.h" 2 3
# 66 "/usr/include/stdlib.h" 2 3
# 68 "/usr/include/stdlib.h" 2 3
# 81 "/usr/include/stdlib.h" 3
# 134 "/usr/include/stdlib.h" 3
# 144 "/usr/include/stdlib.h" 3
# 256 "/usr/include/stdlib.h" 2 3

これがlibディレクトリ以下で起こってしまうので、lib/putenv.c自体はシステムのstdlib.hを見に行ってしまってrpl_putenvが定義されなくなるとかそんなのです。

どう解消するのかというのはまぁ好きにしてくださいって感じだと思うのですが、putenv.cで

/* #include <stdlib.h> /* こっちをコメントアウト */
#include "stdlib.h"

とすれば「取りあえず」動くのでそれで良いと思います。

_environについて

これも結論を言うと、Darwin ldにあるundefinedオプションでdynamic_lookup付けて動的にシンボル解決するようにしろという話です。
_environはcrt1.oでdefinedだというので問題無いと思うのですが、普通このcrt1.oは明示的に渡したりしませんgccが勝手に寄越してくれるので。

まぁつまり

/* env.c */
#include <stdio.h>

void punya(void)
{
    extern char **environ;
    char **strs;
    
    for (strs = environ; *strs != NULL; ++strs)
        printf("%s\n",*strs);
}

/* main.c */
extern void punya(void);

int main()
{
    punya();
    return 0;
}

% gcc -c env.c main.c
% gcc -v main.o env.o
...
 /usr/local/libexec/gcc/x86_64-apple-darwin10/4.6.0/collect2 -dynamic -arch x86_64 -macosx_version_min 10.6.6 -weak_reference_mismatches non-weak -o a.out -lcrt1.10.5.o -L/usr/local/lib -L/opt/local/lib -L. -L/usr/local/lib/gcc/x86_64-apple-darwin10/4.6.0 -L/usr/local/lib/gcc/x86_64-apple-darwin10/4.6.0/../../.. main.o env.o -lgcc_s.10.5 -lgcc_ext.10.5 -lgcc -no_compact_unwind -lSystem
...

% nm /usr/lib/crt1.10.5.o|grep environ 
00000000000000a0 D _environ

ところがMacでdynamic library(つまりdylib)を作る場合は、作る「タイミング」で全シンボルの解決がされないといけないわけなのですが

% gcc -c -fPIC env.c -o env.o
% gcc -v -dynamiclib env.o -o libpunya.dylib
...
/usr/local/libexec/gcc/x86_64-apple-darwin10/4.6.0/collect2 -dynamic -dylib -arch x86_64 -macosx_version_min 10.6.6 -weak_reference_mismatches non-weak -o libpunya.dylib -ldylib1.10.5.o -L/usr/local/lib -L/opt/local/lib -L. -L/usr/local/lib/gcc/x86_64-apple-darwin10/4.6.0 -L/usr/local/lib/gcc/x86_64-apple-darwin10/4.6.0/../../.. env.o -lgcc_s.10.5 -lgcc_ext.10.5 -lgcc -no_compact_unwind -lSystem
...

Undefined symbols:
  "_environ", referenced from:
      _punya in env.o
ld: symbol(s) not found
collect2: ld returned 1 exit status

とcrt1.o渡ってこずにenvironがシンボル解決出来ないので文句を言われます。どうするねんという話なのですが、Darwin ldにはundefinedオプションというものがあり
http://developer.apple.com/library/mac/#documentation/Darwin/Reference/ManPages/man1/ld.1.html

-undefined treatment
                 Specifies how undefined symbols are to be treated. Options are: error, warning, suppress,
                 or dynamic_lookup.  The default is error.
(http://developer.apple.com/library/mac/#documentation/Darwin/Reference/ManPages/man1/ld.1.html より抜粋)

従って

% gcc -dynamiclib env.o -o libpunya.dylib -Wl,-undefined,dynamic_lookup
% gcc main.o libpunya.dylib

と出来ます。

で具体的にguileの場合はどこを弄れば良いのかですけど、libtoolで

# Commands used to build a shared archive.
archive_cmds="\$CC -dynamiclib \$allow_undefined_flag -o \$lib \$libobjs \$deplibs \$compiler_flags -install_name \$rpath/\$soname \$verstring \$single_module~\$DSYMUTIL \$lib || :"

という部分があるので

archive_cmds="\$CC -dynamiclib  -Wl,-undefined,dynamic_lookup \$allow_undefined_flag -o \$lib \$libobjs \$deplibs \$compiler_flags -install_name \$rpath/\$soname \$verstring \$single_module~\$DSYMUTIL \$lib || :"

とかすると良いと思います。

パッチ貼付けた方が良かったですけど元ファイル残してないのでまぁ御免なさいって感じですね。

多分コレで通る

とかそんな感じです。あとはmake checkするなりmake installするなりなんなりと。
ただ、make checkでは幾つかで転けました。

gnuのftpサーバから取って来たguile 2.0ではどうもおかしなエラーが出まくって1日無駄に使ったので避けたとかそんな感じです。

まともな内容のものをあげるところ

http://ranha.kerox.info/gero
ただ例に依って何時飽きるか分かりませんけど、少なくともはてなにこうやって書くよりもまだ人間的なものが書ける気がする。まとまった内容っていうか…

しかしこうWikiとかよりも、テキストファイルとか、pdfを直にあげるほうがスタイリッシュだという思い込みが在るからこれもかなり残念な感じなんだよなーというのがある。
ただ割と昔の役に立つものがテキストファイルで上がってるからって、2011年にそれをやるか??っていうのはあるし、ただまぁテキストファイルだと図を書いたり貼付けるのが面倒臭いんだよなぁというのもあるし。

Google Chromeだと、埋め込みのpdf viewerがあるから割と気軽にpdf見られるしそれでも良いんじゃないかと思うんですけどやっぱりpdfは重い感じあるし、割と抵抗あるよなぁ…。