KERML_ — Problem with nested feature semantics

Consider the following example:

classifier Organization
classifier Car {
    feature drivers : Person; 
}
classifier Person {
    feature employer : Organization [1] {
        feature salary;
    }
    feature drivenCars : Car {
        redefines feature drivers = that;
    }
}

Now assume we have an M0 universe with organization 'bestCorp', a car 'fastCar', and two persons 'joe' and 'jane', filling the values of corresponding features of persons with the instance(s) of matching type. This will give the following extents:

Organization: { (bestCorp), (joe, bestCorp), (jane, bestCorp) }
Car: { (fastCar), (joe, fastCar), (jane, fastCar) ...? }
Person: { (joe, jane), ...? }
employer: { (joe, bestCorp), (jane, bestCorp) }
salary: { (joe, bestCorp, 100000), (jane, bestCorp, 120000) }
drivenCars: { (joe, fastCar), (jane, fastCar) ...? }
Car::drivers: { (joe, fastCar, joe), (jane, fastCar, jane) ...? }
Person::drivenCars::drivers: { (joe, fastCar, joe), (jane, fastCar, jane), ...? }

Some questions that highlight the meaning of this interpretation:

• Who is Joe's employer (i.e., what is the value of joe.employer)?
  • It is bestCorp.
• Do Jane and Joe work at the same company (i.e., jane.employer == joe.employer)?
  • Yes, the values of these features are the same (bestCorp).
• Do Jane and Joe earn the same at bestCorp (i.e., jane.employer.salary == joe.employer.salary)?
  • No, the values of the feature "salary" for (jane, bestCorp) and (joe, bestCorp) are not the same.
• What car does Joe drive (i.e., what is the value of joe.drivenCars)?
  • He drives fastCar.
• Do Jane and Joe drive the same car (i.e., jane.drivenCars == joe.drivenCars)?
  • Yes, the values of these features are the same (fastCar).
• Who are the drivers of Joe's car (i.e., what is the value of joe.drivenCars.drivers)?
  • They are only Joe because Person::drivenCars::drivers maps from a pair of Joe and fastCar to Joe.
• Who are the drivers of Jane's car (i.e., what is the value of jane.drivenCars.drivers)?
  • They are only Jane because Person::drivenCars::drivers maps from a pair of Jane and fastCar to Jane.
• Who are the drivers of fastCar (i.e., fastCar.drivers)?
  • Nobody, because there is no sequence beginning with fastCar.

The last three questions show the unintended behavior, while those with the employer demonstrate that sometimes this is indeed the desired meaning.

Following the terminology of https://conradbock.org/relation3.html, the underlying problem is that drivenCars is interpreted both as a mapping (or relation) from Person to Car and as a role type specializing Car. Features nested under other features could either be interpreted as the feature of the mapping (or relation), or to the role type. This becomes clear if one tries to refactor this to avoid features nested under features by introducing another classifier:

classifier Organization
classifier Car {
    feature drivers : Person; 
}
classifier Employer :> Organization { 
    feature salary;
}
classifier DrivenCar :> Car {
    // ...?
}
classifier Person {
    feature employer : Employer [1];
    feature drivenCars : DrivenCar;
    bind drivenCars.drivers = self;
}

In this case, the extents would look like this:

Organization: { (bestCorp), (joesEmployer), (janesEmployer) }
Car: { (fastCar), (joesCar), (janesCar) ...? }
Person: { (joe, jane), ...? }
employer: { (joe, joesEmployer), (jane, janesEmployer) }
salary: { (joesEmployer, 100000), (janesEmployer, 120000) }
drivenCars: { (joe, joesCar), (jane, janesCar) ...? }
Car::drivers: { (joesCar, joe), (janesCar, jane) ...? }
DrivenCars::drivers: { (joesCar, joe), (janesCar, jane), ...? }

Answers to the above questions change:

• Who is Joe's employer (i.e., what is the value of joe.employer)?
  • It is joesEmployer.
• Do Jane and Joe work at the same company (i.e., jane.employer == joe.employer)?
  • *No, the values of these features are different (janesCorp vs. joesCorp).
• Do Jane and Joe earn the same at bestCorp (i.e., jane.employer.salary == joe.employer.salary)?
  • No, the values of the feature "salary" for janesCorp and joesCorp are not the same, although we do not know that they work at bestCorp (see previous answer).
• What car does Joe drive (i.e., what is the value of joe.drivenCars)?
  • He drives joesCar.
• Do Jane and Joe drive the same car (i.e., jane.drivenCars == joe.drivenCars)?
  • No, the values of these features are different (janesCar vs. joesCar).
• Who are the drivers of Joe's car (i.e., what is the value of joe.drivenCars.drivers)?
  • They are only Joe because his car is joesCar and that is associated only with Joe.
• Who are the drivers of Jane's car (i.e., what is the value of jane.drivenCars.drivers)?
  • They are only Jane because his car is joesCar and that is associated only with Jane.
• Who are the drivers of fastCar (i.e., fastCar.drivers)?
  • Nobody, because there is no sequence beginning with fastCar.