[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
RE: [mizar] Inductive predicates
Dear Adem,
On Wed, 2 Sep 2009, Ozyavas, Adem wrote:
I wrote an evaluator for a functional language called SequenceL in
Mizar. I have some recursive functions in my evaluator whose domains are
very complicated so that their well-definedness proofs are too hard. I
am thinking that writing them as recursive predicates and doing some
proofs about those predicates would be much easier.
I'm not sure if this "workaround" is a good strategy here. It might
happen that when you want to have your article submitted to MML, the
reviewers might complain why some definitions are in the form of
predicates while they should rather be functors...
I believe you should still try to complete the correctness proofs using
this forum, or the Mizar User Service for help to sort out the
particular difficulties in the underlying proofs. But I don't really
know how hard the proofs are, of course :-)
Best,
Adam
=======================================================================
Dept. of Programming and Formal Methods Fax: +48(85)7457662
Institute of Informatics Tel: +48(85)7457559 (office)
University of Bialystok E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================