[Semantics] Think more about whether should embed relational logic, a la Alloy, and how to best combine concrete with symbolic evaluation when it comes to the semantics

[ym-han]

Questions

• Should we remove boolean constants, as Alloy does, so that function expressions cannot return booleans (and so predicates would not be a subtype of functions)?
  • Catala has booleans (as well as booleans with a default value of False)
• How to handle potentially unknown values?
• Should we distinguish between scalars and sets, or not?

Relevant:

Alloy book on scalars

This is a good argument for not having options be a union type for modelling purposes. But not sure it's as persuasive when you're trying to, e.g., write a decision tree like classifier.

p.44-5:

---

Alloy's semantics of integer expressions and formulas

p277

B.7.7 Integers (p 281)

as well as

semantics of integer expressions and formulas

[ym-han]

Papers about Alloy semantics and state:

• Evaluating State Modeling Techniques in Alloy
• Towards an Operational Semantics for Alloy

[ym-han]

TODO: Add docs cataloguing and explaining the differences between Alloy's semantics and Lam4's

EG:

• Sig fields global in Alloy / Forge, but not in Lam4, because (i) evaluating expressions / doing computations is important for Lam4 (ii) global sig fields aren't the best given that