🚀 go-pugleaf

In article <1992Jul19.200646.2244@dscomsf.desy.de>, hallam@zeus02.desy.de (Phillip M. Hallam-Baker) writes:
|> 
|> I have a problem in which I want to build up a master schema from a lot
|> of little ones. The problem is tat a lot of my little schemas are going
|> to be the same. the problem comes when trying to define operations on
|> the composite system which consist of operations on two sub schemas
|> which are essentialy the same.
|> 
|> For example say I have a file server system, I have a schema which
|> defines the state of the file serving robot "ROBOT" and operations
|> "MOVE_ARM_LEFT" "MOVE_ARM_RIGHT" etc. Now the complete system has two
|> robots called Fred and Harry, I want to specify the operation
|> "ALL_WAVE_ARMS" in which Fred does a MOVE_ARM_LEFT and Harry a
|> MOVE_ARM_RIGHT.

If I understand you, your schemas look something like this:

---------------ROBOT-----------------------
| .... schema attributes go here
| ....
|------------------------------------------
| .... schema constraints go here
| ....
-------------------------------------------
 
---------------MoveArmLeft-----------------
| DELTA ROBOT
| ....
-------------------------------------------

---------------MoveArmRight----------------
| DELTA ROBOT
| ....
-------------------------------------------

Fred: ROBOT
Harry: ROBOT

Try redefining your operations this way.

----------------MoveArmLeft-----------------
| r, r': ROBOT
| ...
|-------------------------------------------
| ... state definition of relationship between r and r'
--------------------------------------------

	(and similarly for MoveArmRight)

Then AllWaveArms becomes:

AllWaveArms \defs
	DELTA Fred and DELTA Harry and
		MoveArmLeft[r/Fred][r'/Fred'] and
		MoveArmRight[r/Harry][r'/Harry']

The [a/b] construction is schema renaming, which allows you to rename
the attributes of a schema. They aren't described in Spivey's book (an
oversight on his part, I understand), but fuzz recognizes them.

|> I do remember someone mentioning something about decoration, If I could
|> add have my own decoration sort of "MOVE_ARM_LEFT^{HARRY}"
|> "MOVE_ARM_LEFT^{FRED}" I could squeek by, however this sort of makes me
|> a bit uneasy since I recon that I should then discharge some proof
|> obligation to the effect that the types are compatible and I have a
|> nasty suspicion that there is something lurking...

This is essentially what the above notation does. As far as proof obligation,
what you've said in the statement is textually identical to making two
separate robot-type schemas, and would have exactly the same proof
obligation (basically, that the operations are valid and complete for
the types).

Perhaps I'm showing my Z naivete here, but I don't understand the problem.

Curtis Scott
Carnegie Mellon University
Pittsburgh PA 15221 USA