Find a nicer way to specify (and INTERFACE) Poor Man's Powersets

[WolframKahl]

Thinking about making prerequisites in Hawai more flexible: Why not allow a student to register for destination Hawai if they have passed Surfing, or if they have passed World Religions and History?

Hack:

CONCEPT PrereqGroup  "Poor man's powerset of `Subject`; restricted to non-empty sets"

RELATION inPrereqGroup[Subject * PrereqGroup] [SUR]
MEANING "Membership in `PrereqGroup`; surjective since those sets are non-empty"

POPULATION inPrereqGroup CONTAINS
  [("Surfing", "Surfing")
  ;("World religions","Indigenous culture")
  ;("History","Indigenous culture")
  ]

RELATION required [PrereqGroup * Destination]
POPULATION required CONTAINS
  [("Surfing", "Hawai")
  ;("Indigenous culture", "Hawai")
  ;...
  ]

RULE "Guard Prerequisites" : attends |- (pass~/inPrereqGroup) ; required
MEANING "There is a PrereqGroup all subjects of which are passed."

Conceptually (in a future version of Ampersand 😉 ):

RELATION requires [Destination * Power1 Subject ]
MEANING "`d requires s` means: `d` requires, as one option, all subjects in `s`"

RULE "Guard Prerequisites" : attends |- (pass~/elemPower1);required
POPULATION requires CONTAINS
  [("Hawai", {"Surfing"}))
  ;("Hawai", {"World religions", "History"})
  ;...
  ]

With generic

CONCEPT Power1 X
MEANING "Set of non-empty subsets of `X`"
RELATION elemPower1 [ X * Power1 X ]
MEANING "membership in `Power1 X`"

[sjcjoosten]

I really like the generic pattern, I'm adding a little bit of extra syntax:

PATTERN Power X
  CONCEPT Power1 X
  MEANING "Set of non-empty subsets of `X`"
  RELATION elemPower1 [ X * Power1 X ]
  MEANING "membership in `Power1 X`"
ENDPATTERN

There are several things going on here:

• A pattern is declared with a polymorphic type. The type variable used is X.
• The pattern is bound explicitly in the declaration of the relation requires.
• The pattern is bound implicitly through the use of the relation 'elemPower1'.

Within the pattern, there is a possibility of rules, which makes perfect sense here:

PATTERN Power X
  CONCEPT Power1 X
  MEANING "Set of non-empty subsets of `X`"
  RELATION elemPower1 [ X * Power1 X ]
  MEANING "membership in `Power1 X`"
  RULE ident : I[Power1 X] = elemPower1~ <> elemPower1
  MEANING "Sets are identical iff they contain the same elements"
  PURPOSE "Define the identity on sets. This rule prevents to identical sets from getting different properties when combined with relations outside this pattern."

  RULE empty : elemPower1;'{}'[Power1 X] = -V
  MEANING "No element is in the empty set"
  PURPOSE "Define what it means to be the empty set. With the identity of sets, this uniquely defines the empty set"

  RULE emptyEx : V[ONE*Power1 X];'{}';V = V[ONE]
  MEANING "The empty set exists"
  PURPOSE "Together with the insertEx rule for 'adding' elements to sets, we generate all sets. This rule bootstraps the process."

  RULE insertEx : ???
  MEANING "We can extend a set by a single element"
  PURPOSE "Together with the emptyEx rule for creating the empty set, we generate all sets. This rule says any set can be extended by any element not yet in it."
ENDPATTERN

Sorry for being lazy in the last rule. The above pattern should give rise to all sets of a given type (thanks to concepts being finite). Together with subtyping, we can do dangerous stuff (i.e. stuff of which I don't fully oversee the consequences) like saying (Power1 Set) ISA Set. I guess it's up to the Ampersand user not to get into trouble by doing that.

I don't quite know how to implement a small delta in this direction, but on a whole, it's definitely a direction in which I want to see Ampersand go. It would be nice to see infix names for concepts too, so we can make on-the-fly products, sums, lists... this way too. (Ok, we don't need infix names for this, but it would look nicer)