Constructive Membership Predicates as Index Types

12 years 5 months ago
Constructive Membership Predicates as Index Types
In the constructive setting, membership predicates over recursive types are inhabited by terms indexing the elements that satisfy the criteria for membership. In this paper, we motivate and explore this idea in the concrete setting of lists and trees. We show that the inhabitants of membership predicates are precisely the inhabitants of a generic shape type. We show that membership of x (of type T) in structure S, (x ∈T S) can not, in general, index all parts of a structure S and we generalize to a form ρ ∈ S where ρ is a predicate over S. Under this scheme, (λx.True) ∈ S is the set of all indexes into S, but we show that not all subsets of indexes are expressible by strictly local predicates. Accordingly, we extend our membership predicates to predicates that retain state “from above” as well as allow “looking below”. Predicates of this form are complete in the sense that they can express every subset of indexes in S. These ideas are motivated by experience programmi...
James Caldwell, Josef Pohl
Related Content
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors James Caldwell, Josef Pohl
Comments (0)