Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-31862-0_25 | ICTAC |
Keywords | Field | DocType |
dependent type theory,prolog search algorithm,type family corresponds,inductive definition,surjective random generator,different class,family corresponds,propositional logic,logic program,indexation,search algorithm,dependent types | Inductive logic programming,Discrete mathematics,Second-order logic,Computer science,Zeroth-order logic,Logic programming,Type family,Higher-order logic,Intermediate logic,Dynamic logic (modal logic) | Conference |
Volume | ISSN | ISBN |
3407 | 0302-9743 | 3-540-25304-1 |
Citations | PageRank | References |
1 | 0.36 | 6 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Dybjer | 1 | 540 | 76.99 |
| Qiao Haiyan | 2 | 42 | 3.61 |
| Makoto Takeyama | 3 | 67 | 7.46 |