[Prev][Next][Index]

Re: LSL boolean combinations involving undefined terms

cbj20@veblen (C.B. Jones) writes:

>I recently published a short note on this topic in Information
>Processing Letters. It would be interesting to know what Larch folk
>think about my comments. (Please e-mail - I'm about to be away from
>News for 10 days)

>@article{Jones95e,
>        author   = "C.B. Jones",
>        title    = "Partial functions and logics: A warning",
>        journal  = ipl,
>        volume   = 54, 
>        number   = 2, 
>        pages    = "65--67", 
>        year     = 1995
>}

This is an interesting short article.  I recommend you read it.
Cliff Jones points out that the logic of LSL
can be characterized by the fact that

	e \/ ~e

always holds, even if we don't know the truth of e.
His first example is that if we write...

JonesExample1: trait
  includes Integer
  introduces
    it: -> OneElem
    f: Int -> OneElem
  asserts
    OneElem generated by it
    \forall i: Int
       f(i) == if i=0 then it else f(i-1)

He says that it's not inconsistent that to this trait
one could add:

  implies
    converts f

(that is, f(-1) = it also)
but claims it's surprising to someone who views the trait as defining a
partial function.

I think it would be good to put such an example in reference material
about LSL.  But the conclusion that you'll be surprised if you thought
you were defining a partial function in a language that can only define
total functions seems tautological.

Jones claims that Guttag and Horning do not allow sorts with 1
element, like OneElem.  I've heard something like that,
but is it true?  I should mention that such traits are useful in modelling
things like exception classes with no interesting values...

More interesting is the second example.

JonesExample2: trait
  includes Integer
    fact: Int -> Int
  asserts
    \forall i: Int
       fact(i) == if i=0 then 1 else i * fact(i-1)

A question I have about LSL is:
is there any way to write a provable implication like the following?
 
  implies
    converts fact
      exempting ??????


The problem, Jones says, is that the meaning of this is not the classical
least fixpoint of the definition, because in fact, he notes one can write

  implies
    fact(-1) == - fact(-2)
    fact(-2) == -2 * fact(-2)

and unlike in denotational semantics, none of these are bottom.

One conclusion may be that if you want to get the
least fixpoint, you'd better use a domain, not just Int.
You might use...

Lifted(T): trait
  introduces
    bottom: -> Lift[T]
    inLift: T -> Lift[T]   % will be painful, better in OBJ
    value:  Lift[T] -> T
    proper: Lift[T] -> Bool
    __<__, __<=__: Lift[T],  Lift[T] -> Bool
  asserts
    Lift[T] generated by bottom, inLift
    Lift[T] partitioned by value, proper
    \forall x: T, e, e1: Lift[T]
      proper(e) == e ~= bottom
      value(inLift(x)) = x
      proper(e) => (inLift(value(e)) = e)
      bottom <= inLift(x)
      e <= e
      e < e1 == e <= e1 /\ e ~= e1 
  implies
    % some traits in the handbook and ...
    \forall x: T
      bottom == bottom
      bottom ~= inLift(x)
      proper(inLift(x))
    converts value, proper
      exempting value(bottom)

This gives a certain interpretation of equality on Lift[T],
which I highlight in the implications.
Remember, however, that value(bottom) is some element of T...

So, when we write...

FactTrait: trait
  includes Integer, Lifted(Int)
    fact: Int -> Lift[Int]
  asserts
    \forall i: Int
       fact(i) == inLift(if i=0 then 1 else i * value(fact(i-1)))

expecting that bottom will somehow be used as the value of
fact(-1), we are disappointed.  fact(-1) is a (proper)
integer, because value(bottom) is some element of Int.
We might try adding the equation...
       fact(-1) == bottom
but this leads to inconsistency, as shown by the following calculation.

	  bottom
	=   {by the new equation}
	  fact(-1)
        =   {by the equation in FactTrait} 
          inLift(if -1=0 then 1 else -1 * value(fact(-1-1)))
	=   {by def of if}
	  inLift(-1 * value(fact(-1-1)))
	~=   {by the trait Lifted, see the second implication}
	  bottom

Instead, we have to define fact as follows, if we want the
least fixpoint. 

FactTrait: trait
  includes Integer, Lifted(Int)
    fact: Int -> Lift[Int]
  asserts
    \forall i: Int
       fact(i) == if i < 0 then bottom
                  else if i=0 then 1 else inLift(i * value(fact(i-1)))

One could let that stand as the objection Jones raises:
if you want to define least fixpoints, it's better to work in
a language that supports a notion of partiality.

	Gary Leavens
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html
Follow-Up(s): Reference(s):