RE: 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: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================