Re: TYPOL-Properties

[ia@trinidad.inria.fr (Isabelle Attali)]

In article 183 of sophia.centaur, kuehne@isa.informatik.th-darmstadt.de 
(Thomas Kuehne) writes:

=> Am i right to assume, that the rule
=>
=> MapRest |- Pid -< Paccess : Result
=> --------------------------------------------------------------------------
=> pmap[paccess(pdef(proc_def(proc_header(Pid', _, _), _, _)), _).MapRest] |- 
=>   Pid -< Paccess : Result;
=>   provided diff(Pid', Pid);

=> does not violate the link-less condition, although Pid and Pid' are linked 
=> via the predicate "diff".
=> But Pid is not in the set of the input attribute and that is why the rule
=> is still link-less to my understanding.
=> Is that true?

I must admit that I do not really understand your rule:
what is known during proofs, where is the subject,
why two relations in the sequent ?
May I suggest that the subject in not Pid but pmap[...] ??

Following our terminology, we try to give the TYPOL rules the form:

	H1 |- T1 : S1   ...   Hn |- Tn : Sn
	-----------------------------------
		H |- T : S

where:
	T, Ti are subjects (abstract syntax trees of a language)
	S, Hi are output attributes (computed in the rule with input attributes)
	H, Si are input attributes (computed elsewhere and used in this rule)

You may re-formulate your rule with:

    MapRest |- Pid -< Paccess , Result
(1) --------------------------------------------------------------------------
    pmap[paccess(pdef(proc_def(proc_header(Pid', _, _), _, _)), _).MapRest] |- 
      Pid -< Paccess , Result;
      provided diff(Pid', Pid);
	
or:

    Pid |- MapRest -< Paccess , Result
(2) --------------------------------------------------------------------------
    Pid |- 
	pmap[paccess(pdef(proc_def(proc_header(Pid', _, _), _, _)), _).MapRest]
          -< Paccess , Result;
     provided diff(Pid', Pid);

with only one relation in the sequent.

(1) and (2) are link-less (with no common variable between input attributes)

(1) is not constraint-less but (2) is.

These two properties are automatically checked by my own type-checker
(not yet part of the official release of Centaur).

You can transform the rule by changing the subject (without the help of 
another set) as in rule (2).

Anyway, these two properties are not needed to get a functional evaluation 
of Typol programs (but to get an attribute grammar).

For a functional evaluation, the hypotheses are :
- the "safe" property (output attributes are given in terms of input 
	attributes)
- the strongly non circular property (there exists an order in premises).

Sorry for the delay in the answer.

Isabelle Attali