strict/lazy reasoning
Download
Report
Transcript strict/lazy reasoning
Reasoning about explicit strictness
in a lazy language
using mixed lazy/strict semantics
Marko van Eekelen
Maarten de Mol
Nijmegen University, NL
Technical Report NIII-R0402
(Revised Version at www.cs.kun.nl/~marko/research)
Not NIII-R 0408, 0415, 0416, 0427, …
June 21, 2004
1
Lazy semantics need to be extended
Overview
• The Sparkle project:
integrating programming and theorem proving
focus on functional programming
• Some lazy/strict reasoning principles with
• The strictness gap:
programmers versus theoreticians
• Some basic reasoning examples
• The basis of strictness constructs in lazy languages
• Mixed lazy/strict semantics
• Conclusions and Future work
June 21, 2004
2
The Sparkle Project:
Theorem Proving for Programmers
Function(s)
Sparkle:
dedicated
proof assistant
Properties
Program
with
proof
certificate
Clean Compiler
Semantic reasoning level is the semantics of the programming language
June 21, 2004
3
Extensionality:
Now:
Since the meaning of both
and
is undefined.
So,
and
are semantically equal for each .
However, is in head normal form and is
undefined:
So, and are not equal.
An extra condition is needed (Abramsky):
June 21, 2004
4
Induction
Due to laziness an extra base step
for the undefined case is required.
y[A]: P (y)
• P()
• P([])
• xAxs[A]: P (xs) P([x:xs])
Without this extra step we could
e.g. easily prove that every list is finite.
Furthermore, P has to be admissible (Paulson).
June 21, 2004
5
The strictness gap
• Theoreticians view on strictness:
A derived formal property
– Mathematical property of semantic function definitions
– Undecidable property, approximated via a safe analysis using
abstract interpretation, abstract reduction or some type inference
system
• Programmers view on strictness:
A programming decision
– Essential for efficiency of data structures
– Essential for efficiency of evaluation
– Essential for enforcing the evaluation order in interfaces
But programmer defined strictness has an effect on definedness.
June 21, 2004
6
Closing the gap
• Mathematical view on strictness:
x=fx=
• Operational view on strictness:
Reduce argument to weak head normal form
before evaluating the function application
• Notation for Strictness:
Merely annotation, no semantics
• Mixed semantics:
Notationally strict => operationally strict => mathematically strict
• For reasoning a mixed strict/lazy graph rewriting
semantics is needed
June 21, 2004
7
Basic lazy-strict reasoning - 1
Reasoning about Clean functions:
Strict equality:
Lazy and:
Lazy or:
==
True ==
&&
False &&
||
True ||
True
False
True
is
is
is
is False
is
is True
Reasoning on the predicate level:
Logical identity:
True
Logical and:
= True
True
Logical or:
True
June 21, 2004
True
True
True
True
is False
is False
is ill-formed but used as shorthand for:
is False
is False
is True
is True
8
Basic lazy-strict reasoning - 2
Consider the following property
It is not valid if both x and y are !
What does hold is the following:
Many properties do hold unconditionally, e.g:
June 21, 2004
9
A property of isMember
•
•
•
•
•
x =
x
x =
x =
...
,
,
2,
2,
xs
xs
xs
xs
June 21, 2004
=
=
=
[ ],
[, x],
[2:xs],
[3],
p
p
p
p
y
y
y
y
=
=
=
=
False
False
False
if (y == 2) True (p y)
10
A case for which P does not hold
x = 2, xs = [3], p y = if (y == 2) True (p y)
Then:
• p x = True
• isMember x xs = False
• filter p xs = []
• isMember x (filter p xs) =
So, P(x,xs,p):=
= False && True
Hence P does not hold in this case.
June 21, 2004
11
How to express this in Sparkle, which is first order?
June 21, 2004
12
Expressing Properties
Definedness of an object x:
Totality of a predicate p:
Finiteness of lists:
The auxiliary function to express finiteness of lists:
June 21, 2004
13
The basic construct: let!
•
•
•
•
(partially) strict data structures
user annotated function arguments
unboxed arrays
special primitives like seq or #!
They can all be expressed easily with a single construct,
the let!-construct:
Lazy semantics must be extended
to express the meaning of let!.
June 21, 2004
14
Launchbury’s semantics
June 21, 2004
15
Extra rule for mixed semantics
June 21, 2004
16
Basic Idea
June 21, 2004
17
Define Meaning
Lazy Semantics:
Extra rule for mixed semantics:
June 21, 2004
18
Proving Mixed Semantics
Correctness
Computational Adequacy
June 21, 2004
19
Folklore Strictness Knowledge
A. Expressions that are bottom lazily, will also
be bottom when we make something strict.
B. When strictness is added to an expression
that is non-bottom lazily, either the result
stays the same or it becomes bottom.
C. Expressions that are non-bottom using
strictness will (after !-removal) also be
non-bottom lazily with the same result.
June 21, 2004
20
Switching from
Mixed to Lazy Semantics
Expressions:
Environments:
June 21, 2004
21
Formal Strictness Knowledge
June 21, 2004
22
Distinguishing different terms
• In Launchbury’s lazy semantics
and
have a different meaning
but they can not be distinguished.
• With mixed semantics
and
are different and they can be distinguished.
June 21, 2004
23
Conclusions/Future Work
Conclusions
• Mixed semantics are needed for reasoning
in Haskell and Clean
• Mixed semantics essentially extend lazy
semantics
Future Work
• Extend mixed graph rewriting semantics
extend the logic with single step semantics
• Full Integration of prover and language
towards programming with proven properties
June 21, 2004
24