From c3b4c7aee1f0d4beb078938d330e982e752927a1 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 01:06:21 -0300 Subject: decision 14: no application in term position, spec example rewritten flat --- docs/language-specification.org | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'docs/language-specification.org') diff --git a/docs/language-specification.org b/docs/language-specification.org index 9158130..639e8d6 100644 --- a/docs/language-specification.org +++ b/docs/language-specification.org @@ -1152,12 +1152,20 @@ For example: #+BEGIN_SRC sol [ForAll variable: X quantifier: [Integer value: X] - body: - [Equal left: [Plus left: X right: 0] right: X]] + body: [Plus left: X right: 0 result: X]] #+END_SRC +This says that the tuple ={left: X, right: 0, result: X}= belongs to +=Plus= for every integer =X=: the identity law stated as membership. +Note what it is not written as: =[Equal left: [Plus left: X right: 0] +right: X]=, with an application nested in term position. That form is +rejected. A block is a proposition, never a value; treating it as a +value would require privileging one attribute as "the" result, and a +relation has no distinguished output. The flat membership form is +both the honest one and the shorter one. + This should be proved symbolically, by the algebraic properties of -=Plus= and =Equal=, not by checking every integer. +=Plus=, not by checking every integer. If Sol cannot prove such a universal symbolically, it must reject the program, keep it as an unproven obligation, or require an explicit -- cgit v1.2.3