[SCL] Suggestion for SCL extension module

[pat hayes]

>Chris,
>
>Hopefully we can get your version very soon now:
>we'll have some work to do on full SCL modules
>and SCL concrete syntaxes, which cannot be really
>started before.
>
>Meanwhile I have a proposal about a full SCL
>module, which we could include. We have spoken
>about it before, but IMHO too little.
>

....

>Finally, perhaps the same goals could be achieved
>using the annotations module in the SCL.
>Remember: "formula_3(annot,something,f1)"
>is equivalent to "f1"
>and "term_3(annot,something,t1)"
>is equal to "t1".
>
>I have not really thought yet whether
>the annotation module would be enough
>or not.
>
>Any thoughts on this theme?

1. I like the overall idea  and indeed had been thinking along similar lines.

2. However, Im not sure about the 'proposition skolemization' trick 
you suggest.

3. In the short term, we could keep a slot open for this by simply 
weakening the syntactic conformance requirements to allow 
non-well-formed SCL to occur in an SCL document without breaking it. 
This allows us to return to this later.  Many users will not like 
that option, so it will need to be an option.

4. Re. using annotations, we could handle any 'alien' operator by 
moving it and all its subexpressions into an annotation, and 
replacing the entire expression with the a new Skolemized dummy 
expression of the appropriate syntactic type, with this as its 
annotation. That could be a 'standard' way to encode such things 
without breaking the SCL syntax rules, though it would not itself 
capture the intended meaning.

5. We might be able to do better for the common cases. What do we 
need? Suppose we allow a single new syntactic category of 'opaque 
operator', which can be wrapped around any sentence. Then non-mon can 
be handled by an opaque negation, modalities are opaque, and any 
procedural call-out that affects logical meaning can be enclosed in 
an opaque annotation wrapper. This might be sufficient: then we can 
treat the opaque-enclosed subexpression as an atom in its own right 
as far as pure SCL is concerned. It would be nice if we could state a 
requirement along the lines that any SCL *inside* the opaque wrapper 
should inherit that same meaning that it has outside, but I don't see 
any way to state that at present with enough generality. (Its easy 
enough for non-mon, but not for modalities.)

Pat

>Regards,
>          Tanel Tammet
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes