CODEWITHSUNDEEP
z3smt
JRR
JRR

Reputation: 6152

does smtlib support first class functions?

Say for modeling the haskell map function, which takes in a "mapper" function that is applied to all elements of a list. How can I declare map in smtlib?

Upvotes: 1

Views: 78

Answers (1)

alias
alias

Reputation: 30525

No; SMTLib is essentially a first-order theory; higher order functions are simply not supported.

Z3, however, allows mapping functions over arrays, with the (_ map f) extension. See https://rise4fun.com/Z3/tutorial/guide, search for "Mapping Functions on Arrays." This doesn't give you arbitrary higher-order functions, but can be used to simulate those that operate on SMTLib arrays.

If you do intend to reason about higher-order functions, then SMTLib is arguably the wrong logic for you. Use of a more traditional theorem prover like HOL/Isabelle, or modern incarnations in Agda/Coq would be more suitable. You can also take a look at Lean, which has a good compromise of features and automation.

Upvotes: 1

Related Questions