Stream: Beginner Questions

Topic: Question about the type

Hongjian Jiang (Jul 16 2023 at 09:21):

theory Regular_Exp
imports Regular_Set
begin

datatype (atoms: 'a) rexp =
  is_Zero: Zero |
  is_One: One |
  Atom 'a |
  Plus "('a rexp)" "('a rexp)" |
  Times "('a rexp)" "('a rexp)" |
  Star "('a rexp)"


instantiation rexp :: (order) "{order}"
begin
...
end

For the code above, I have several misunderstanding.

1. why atoms in datatype could return a set, in the tutorial the parameter just means the variable.
2. What is the role of first and second order in the class instantiation.

Hongjian Jiang (Jul 16 2023 at 12:27):

any helps would be appreciated

Mathias Fleury (Jul 16 2023 at 12:35):

I have no clue what you are talking about. In

instantiation rexp :: (order) "order"

If you think about applying it to 'a rexp: The first (order) is a constraint about 'a (in this case, 'a must be equipped with an order) and the second order is the constraint you add to rexp. In this case if the case type has an order, then rexp also has an order

Hongjian Jiang (Jul 16 2023 at 13:11):

Thank you very much. You mean every rexp here is type order now like Zero is an order, One is an order.

And rexp is a name of order class.

What is the function of is_Zero, is_One and atoms play in the datatype.

Mathias Fleury (Jul 16 2023 at 13:14):

No, this is not what I mean…

Mathias Fleury (Jul 16 2023 at 13:14):

Zero and One are elements of a type called rexp parametrized by another type

Mathias Fleury (Jul 16 2023 at 13:16):

and is_Zero and is_One are discriminators (see here)

Mathias Fleury (Jul 16 2023 at 13:17):

and atoms returns the set of all atoms in the rexp formula

Last updated: Apr 28 2024 at 08:19 UTC