11
$\begingroup$

Say I'm formalizing something in group theory, and I'm working with some action $\cdot$ of $(G, +)$ on a set. In my math textbook, the identity of $\cdot$ is explicitly mentioned once (if that), and then left implicit. In my formalization, do I have to constantly keep specifying $(G, \cdot)$, or can I temporarily set $\cdot$ as the default?

In my limited experience, mathematical writing uses "dynamic scope" like this a lot. Does this actually correspond to a computer scientist's definition of dynamic scope, and if so, do any proof assistants support this?

$\endgroup$
8
  • $\begingroup$ The way to do something like this depends a lot on your proof assistant. For instance, Coq has sections and modules; Agda has a different sort of module. $\endgroup$ Feb 11 at 18:42
  • $\begingroup$ IIRC, ACL2 has the same dynamic scoping of Common Lisp. $\endgroup$ Feb 11 at 18:43
  • $\begingroup$ I think you just need to find your proof assistant where you will be satisfied with the look of theorems. There is no so called right way to implement abstract algebra library. It is more like market where you choose. $\endgroup$ Feb 11 at 18:46
  • 5
    $\begingroup$ This is, imo, a way to specify local instances, not the "dynamic scoping" in traditional PL sense $\endgroup$
    – ice1000
    Feb 11 at 18:48
  • $\begingroup$ It is not clear from your question which of several proof assistant techniques suits your needs. You could be asking whether you can mention the neutral element without mentioning the group. You could be asking whether you can construct a group without specifying the unit. Or maybe you just want to say "whenever you see variable x assume its type is t" (which is how people are interpreting your question). It would be helpful if you gave a specific example of what you'd like. Also, what you are looking for is not called dynamic scope. $\endgroup$ Feb 12 at 8:48

2 Answers 2

3
$\begingroup$

Agda has generalization of declared variables. In short, you can leave a variable block of variables that are appearing often.

Example:

variable
  g : Grammar

first-item : symbol g -> Item g

It implicitly adds the {g:Grammar} -> in front of the first-item.

There's another system that lets you do this on variables, called modules. And here's an example of using that:

module FinMap (k : Set)
              (size : ℕ) where
   maxSize : ℕ
   maxSize = size

You can later open this kind of a module and fill in the pieces. Possibly within another module, if your fill-up depends on implicits.

module ItemSet {g : Grammar} {n : ℕ} where
  open FinMap.FinMap (EIM g n) (eim-size g n) public
    using (maxSize)

These are syntactic-sugar features relying on implicits. It behaves a lot like a dynamic scope in practice.

$\endgroup$
2
  • $\begingroup$ This looks a lot like how variables and modules work in Coq (I think)... but it hadn't occurred to me to emulate "local instances" in this way. I come from Haskell, so I'm still trying to wrap my head around ML-like modules :-) Purely out of curiosity, does Agda use typeclasses as well as modules—and if so, is there a solution like this for them as well? $\endgroup$ Feb 13 at 16:22
  • $\begingroup$ @JoshuaGrossoReinstateCMs Agda has typeclasses as well, but I don't know how do they work. manual page: agda.readthedocs.io/en/v2.6.2.1/language/… $\endgroup$
    – Cheery
    Feb 13 at 17:15
3
$\begingroup$

In Isabelle/Isar locale can be used to specify implicit assumptions and notation conventions that are limited in scope. The assumptions are then added to each theorem proven in the locale. With the sublocale keyword one can define how notation maps from one context (locale) to another so that theorems can be reused in a different context.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.