Do Expressions and Formulae really need to be separated ?

GillianPlatform / Gillian

The Gillian Platform main repository

https://GillianPlatform.github.io

BSD 3-Clause "New" or "Revised" License

78 stars 11 forks source link

Do Expressions and Formulae really need to be separated ? #6

Closed giltho closed 1 year ago

giltho commented 4 years ago

Formulae are just boolean expressions + ForAll They could probably be simplified A LOT, if Expressions were GADTs that can be determined to be boolean expressions at compilation time. The Formula would be something like:

| Pure of expr
| Forall of (var * type opt) list * expr

giltho commented 1 year ago

I will close this issue as I believe this would be part of a bigger work on the theory of CSE. My current intuition is that symbolic values should allow for forall and formulae are not really a thing.