Define mutually recursive functions in SMTLIB 3.0?

33 views
Skip to first unread message

Siyuan Chen

unread,
Oct 12, 2021, 5:04:47 AM10/12/21
to SMT-LIB
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

unread,
Nov 1, 2021, 11:08:10 AM11/1/21
to smt...@googlegroups.com, Siyuan Chen
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

unread,
Nov 1, 2021, 4:44:58 PM11/1/21
to smt...@googlegroups.com, Siyuan Chen
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

Reply all
Reply to author
Forward
0 new messages