5

Following up from my recent question, I have been pondering over the following:

We can create some new amazing types in LH, particularly, express some non-trivial subsets of Integers. For example:

{-@ type Nat = {v:Int | v>=0 } @-}
{-@ type grtN N = {v:Int | v>N } @-}
{-@ type Even = {v:Int | v mod 2 == 0 } @-}

But now what other non-trivial subsets can I express in LH?

Can I create a type in LH which consists of only powers of 2? Which is what my last question was about and it seems like the answer is negative.

So a natural question which arises is what kind of subsets (of Integers) can I express? Is there a nice characterization?

kishlaya
  • 453
  • 2
  • 14

1 Answers1

2

I believe that LH will let you write arbitrary arithmetic constraints. But only the theory of linear integer arithmetic is decidable (via presburger arithmetic) by the backend solver, so as soon as you start writing non-linear expressions you lose any guarantee that the solver will actually verify your code. Additionally, SMT solvers only support first-order logic, so you can't quantify over relations.

trpnd
  • 455
  • 2
  • 10