Define mutually recursive functions in SMTLIB 3.0?

[Siyuan Chen]

Dear SMT community,

I just read the SMT-LIB v3.0 preliminary proposal (http://smtlib.cs.uiowa.edu/version3.shtml). It is so powerful. I am very looking forward to this version!

However, it does not seem to support defining mutually recursive functions? 

The `define-funcs-rec` will still be reserved? Or need to introduce a new syntax (e.g. `and` in SML) or support forward reference in `lambda` like Scheme.

Thanks.

[Pascal Fontaine]

Dear Siyuan Chen,

On 10/12/21 11:04 AM, Siyuan Chen wrote:

Dear SMT community,

I just read the SMT-LIB v3.0 preliminary proposal (http://smtlib.cs.uiowa.edu/version3.shtml). It is so powerful. I am very looking forward to this version!

However, it does not seem to support defining mutually recursive functions?

The document http://smtlib.cs.uiowa.edu/version3.shtml only focusses on what is changing with respect to version 2.6.  There is no plan to remove features, and in particular, mutually recursive functions will still be there.

Best,

  Pascal (also for Cesare and Clark)

The `define-funcs-rec` will still be reserved? Or need to introduce a new syntax (e.g. `and` in SML) or support forward reference in `lambda` like Scheme.

Thanks. --
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/57cd2c95-63eb-41bc-86b5-821ef257045dn%40googlegroups.com.

[Viktor Kunčak]

The expanding definition of SMT-LIB 3.0 continues to be exciting to me. :)

It says somewhere that it will have "classical semantics". What does that mean?

There is an example with 'Type'. What is the interpretation of 'Type'?

Do we expect to have set theoretic semantics from inside Zermelo-Fraenkel set theory

or maybe already Zermelo set theory alone would suffice, as for HOL ?

Thanks,

  Viktor

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/d8ff994f-e37d-f6be-220f-0723d81b7451%40uliege.be.