研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	英語
発行・発表の年月	2005
形態種別	学術雑誌
査読	査読あり
標題	Random Generators for Dependent Types
執筆形態	共著
掲載誌名	ICTAC 2004 Revised selected Papers, Lecture Notes in Computer Science, vol.3407
掲載区分	国外
巻・号・頁	pp.341-355
著者・共著者	Peter Dybjer, Qiao Haiyan, Makoto Takeyama
概要	We show how to write surjective random generators for several different classes of inductively defined types in dependent type theory. We discuss both non-indexed (simple) types and indexed families of types. In particular we show how to use the relationship between indexed inductive definitions and logic programs: the indexed inductive definition of a type family corresponds to a logic program, and generating an object of a type in the family corresponds to solving a query for the logic program. As an example, we show how to write a surjective random generator for theorems in propositional logic by randomising the Prolog search algorithm.