[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
>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

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):