In natural deduction, is there a word for a bunch of related formation, introduction, elimination, and computation rules? Examples would be: pairs, functions, records, etc. I think some would call these 'types' but somehow I feel that only covers the type constructor part.
Conversation
Replying to
the ones you described are all the result of embedding some algebraic laws into the rules, right? i wonder if universal algebra is a useful frame here
1
1
what does plt redex call them internally, if anything?
1
Show replies
Replying to
Isabelle organises proofs into ‘theories’, which are essentially modules, but that might be broader than what you mean here?
2
1
Yeah I think it's a similar problem here: twitter.com/brendanzab/sta - like, I want to talk about specific 'language feature', like the function arrow+lambda+application+beta reduction together as a single thing.
Quote Tweet
Replying to @JohnMeuser
Doesn't 'framework' refer to the collection of different features however? Or are you talking about having a framework that has only a 'pair' defined, and 'function' defined, then somehow smooshing them together to form another, larger framework?
1
1
Show replies
Replying to
No, sorry, computer science has officially run out of words for groups or classes of things.
2
1
Replying to
No standard word, but I'd say "the function-type rules" or "the rules governing each connective", etc. I think it's fine in context to say "the function type" (part of being a type is having a notion of element) but it's easily misunderstood.