From 796d8ced7eb30bcd4357093742a141171aa8bd26 Mon Sep 17 00:00:00 2001 From: Vik Fearing Date: Thu, 10 Sep 2026 14:31:03 +0200 Subject: [PATCH v2 2/2] Add the IMPLIES boolean operator a IMPLIES b is material implication, parsed as a right-associative operator binding below OR and expanded to NOT a OR b in the parser, so type errors are reported against IMPLIES itself. Because NOT and OR are already Kleene operators, that expansion settles the three-valued truth table on Kleene implication, where Unknown IMPLIES Unknown is Unknown. SQL has until now used only the fragment of three-valued logic on which Kleene and Lukasiewicz agree, and implication is exactly where the two differ: Lukasiewicz would make Unknown IMPLIES Unknown be True, which could not then be written as NOT a OR b. Right associativity makes a chain equivalent to a single implication whose antecedent is the conjunction of the leading operands, so a IMPLIES b IMPLIES c is (a AND b) IMPLIES c. --- doc/src/sgml/func/func-logical.sgml | 80 ++++++++++++++ doc/src/sgml/syntax.sgml | 6 ++ src/backend/nodes/outfuncs.c | 4 + src/backend/nodes/readfuncs.c | 5 + src/backend/parser/gram.y | 11 +- src/backend/parser/parse_expr.c | 35 ++++++ src/include/nodes/parsenodes.h | 1 + src/include/parser/kwlist.h | 1 + src/test/regress/expected/boolean.out | 149 ++++++++++++++++++++++++++ src/test/regress/sql/boolean.sql | 60 +++++++++++ 10 files changed, 351 insertions(+), 1 deletion(-) diff --git a/doc/src/sgml/func/func-logical.sgml b/doc/src/sgml/func/func-logical.sgml index 5ba6389db56..4769202e805 100644 --- a/doc/src/sgml/func/func-logical.sgml +++ b/doc/src/sgml/func/func-logical.sgml @@ -39,10 +39,19 @@ negation + + IMPLIES + + + + implication + + boolean AND boolean boolean boolean OR boolean boolean NOT boolean boolean +boolean IMPLIES boolean boolean SQL uses a three-valued logic system with true, @@ -146,6 +155,77 @@ + + The IMPLIES operator is material implication: + a IMPLIES + b is equivalent to NOT + a OR + b, and reads as if + a then b. + Unlike AND and OR it is not + commutative, which is why its table, unlike theirs, is not symmetric + about the diagonal: + + + + + + IMPLIES + True + False + Unknown + + + + + + True + True + False + Unknown + + + + False + True + True + True + + + + Unknown + True + Unknown + Unknown + + + + + + + + IMPLIES binds less tightly than every other operator, + OR included, and it is right-associative, so + a = 1 IMPLIES b = 2 IMPLIES c = 3 means + (a = 1) IMPLIES ((b = 2) IMPLIES (c = 3)). See . + + + + Chaining implications is therefore the same as a single implication whose + antecedent is the conjunction of the leading operands: + a IMPLIES + b IMPLIES + c is equivalent to + (a AND + b) IMPLIES + c. It is not equivalent to + a IMPLIES + (b AND + c); that meaning has to be written with + explicit parentheses. + + The operators AND and OR are commutative, that is, you can switch the left and right operands diff --git a/doc/src/sgml/syntax.sgml b/doc/src/sgml/syntax.sgml index 67482996861..bee928a8414 100644 --- a/doc/src/sgml/syntax.sgml +++ b/doc/src/sgml/syntax.sgml @@ -1103,6 +1103,12 @@ CAST ( 'string' AS type ) left logical disjunction + + + IMPLIES + right + logical implication + diff --git a/src/backend/nodes/outfuncs.c b/src/backend/nodes/outfuncs.c index 40990143927..9a35ff53de0 100644 --- a/src/backend/nodes/outfuncs.c +++ b/src/backend/nodes/outfuncs.c @@ -643,6 +643,10 @@ _outA_Expr(StringInfo str, const A_Expr *node) appendStringInfoString(str, " NOT_BETWEEN_SYM"); WRITE_NODE_FIELD(name); break; + case AEXPR_IMPLIES: + appendStringInfoString(str, " IMPLIES"); + WRITE_NODE_FIELD(name); + break; default: elog(ERROR, "unrecognized A_Expr_Kind: %d", (int) node->kind); break; diff --git a/src/backend/nodes/readfuncs.c b/src/backend/nodes/readfuncs.c index 2839a711f9e..4cc019a012b 100644 --- a/src/backend/nodes/readfuncs.c +++ b/src/backend/nodes/readfuncs.c @@ -514,6 +514,11 @@ _readA_Expr(ReadNodeContext *ctx) local_node->kind = AEXPR_NOT_BETWEEN_SYM; READ_NODE_FIELD(name); } + else if (length == 7 && strncmp(token, "IMPLIES", 7) == 0) + { + local_node->kind = AEXPR_IMPLIES; + READ_NODE_FIELD(name); + } else if (length == 5 && strncmp(token, ":name", 5) == 0) { local_node->kind = AEXPR_OP; diff --git a/src/backend/parser/gram.y b/src/backend/parser/gram.y index 0563453fe24..cd70db96c61 100644 --- a/src/backend/parser/gram.y +++ b/src/backend/parser/gram.y @@ -749,7 +749,8 @@ static Node *makeRecursiveViewSelect(char *relname, List *aliases, Node *query); HANDLER HAVING HEADER_P HOLD HOUR_P - IDENTITY_P IF_P IGNORE_P ILIKE IMMEDIATE IMMUTABLE IMPLICIT_P IMPORT_P IN_P INCLUDE + IDENTITY_P IF_P IGNORE_P ILIKE IMMEDIATE IMMUTABLE IMPLICIT_P IMPLIES + IMPORT_P IN_P INCLUDE INCLUDING INCREMENT INDENT INDEX INDEXES INHERIT INHERITS INITIALLY INLINE_P INNER_P INOUT INPUT_P INSENSITIVE INSERT INSTEAD INT_P INTEGER INTERSECT INTERVAL INTO INVOKER IS ISNULL ISOLATION @@ -844,6 +845,7 @@ static Node *makeRecursiveViewSelect(char *relname, List *aliases, Node *query); /* Precedence: lowest to highest */ %left UNION EXCEPT %left INTERSECT +%right IMPLIES %left OR %left AND %right NOT @@ -15374,6 +15376,11 @@ a_expr: c_expr { $$ = $1; } { $$ = makeAndExpr($1, $3, @2); } | a_expr OR a_expr { $$ = makeOrExpr($1, $3, @2); } + | a_expr IMPLIES a_expr + { + $$ = (Node *) makeSimpleA_Expr(AEXPR_IMPLIES, "IMPLIES", + $1, $3, @2); + } | NOT a_expr { $$ = makeNotExpr($2, @1); } | NOT_LA a_expr %prec NOT @@ -18190,6 +18197,7 @@ unreserved_keyword: | IMMEDIATE | IMMUTABLE | IMPLICIT_P + | IMPLIES | IMPORT_P | INCLUDE | INCLUDING @@ -18782,6 +18790,7 @@ bare_label_keyword: | IMMEDIATE | IMMUTABLE | IMPLICIT_P + | IMPLIES | IMPORT_P | IN_P | INCLUDE diff --git a/src/backend/parser/parse_expr.c b/src/backend/parser/parse_expr.c index 05a6b72d4c9..3f9dc86fa00 100644 --- a/src/backend/parser/parse_expr.c +++ b/src/backend/parser/parse_expr.c @@ -54,6 +54,7 @@ static Node *transformAExprDistinct(ParseState *pstate, A_Expr *a); static Node *transformAExprNullIf(ParseState *pstate, A_Expr *a); static Node *transformAExprIn(ParseState *pstate, A_Expr *a); static Node *transformAExprBetween(ParseState *pstate, A_Expr *a); +static Node *transformAExprImplies(ParseState *pstate, A_Expr *a); static Node *transformMergeSupportFunc(ParseState *pstate, MergeSupportFunc *f); static Node *transformBoolExpr(ParseState *pstate, BoolExpr *a); static Node *transformFuncCall(ParseState *pstate, FuncCall *fn); @@ -213,6 +214,9 @@ transformExprRecurse(ParseState *pstate, Node *expr) case AEXPR_NOT_BETWEEN_SYM: result = transformAExprBetween(pstate, a); break; + case AEXPR_IMPLIES: + result = transformAExprImplies(pstate, a); + break; default: elog(ERROR, "unrecognized A_Expr kind: %d", a->kind); result = NULL; /* keep compiler quiet */ @@ -1446,6 +1450,37 @@ transformBoolExpr(ParseState *pstate, BoolExpr *a) return (Node *) makeBoolExpr(a->boolop, args, a->location); } +/* + * Transform "a IMPLIES b" into the equivalent "NOT a OR b". + * + * We expand this here rather than in gram.y so that a non-boolean operand is + * complained of in terms of IMPLIES, rather than in terms of the NOT or OR + * that the construct happens to be built from. + */ +static Node * +transformAExprImplies(ParseState *pstate, A_Expr *a) +{ + Node *lexpr; + Node *rexpr; + + lexpr = transformExprRecurse(pstate, a->lexpr); + rexpr = transformExprRecurse(pstate, a->rexpr); + + lexpr = coerce_to_boolean(pstate, lexpr, "IMPLIES"); + rexpr = coerce_to_boolean(pstate, rexpr, "IMPLIES"); + + /* + * Each operand appears exactly once in the expansion, so unlike BETWEEN + * this does not risk evaluating anything twice. + */ + return (Node *) makeBoolExpr(OR_EXPR, + list_make2(makeBoolExpr(NOT_EXPR, + list_make1(lexpr), + exprLocation(lexpr)), + rexpr), + a->location); +} + static Node * transformFuncCall(ParseState *pstate, FuncCall *fn) { diff --git a/src/include/nodes/parsenodes.h b/src/include/nodes/parsenodes.h index 0debcd193ab..45fa8c70263 100644 --- a/src/include/nodes/parsenodes.h +++ b/src/include/nodes/parsenodes.h @@ -342,6 +342,7 @@ typedef enum A_Expr_Kind AEXPR_NOT_BETWEEN, /* name must be "NOT BETWEEN" */ AEXPR_BETWEEN_SYM, /* name must be "BETWEEN SYMMETRIC" */ AEXPR_NOT_BETWEEN_SYM, /* name must be "NOT BETWEEN SYMMETRIC" */ + AEXPR_IMPLIES, /* name must be "IMPLIES" */ } A_Expr_Kind; typedef struct A_Expr diff --git a/src/include/parser/kwlist.h b/src/include/parser/kwlist.h index 53ae96c0399..94d2aef1bb1 100644 --- a/src/include/parser/kwlist.h +++ b/src/include/parser/kwlist.h @@ -207,6 +207,7 @@ PG_KEYWORD("ilike", ILIKE, TYPE_FUNC_NAME_KEYWORD, BARE_LABEL) PG_KEYWORD("immediate", IMMEDIATE, UNRESERVED_KEYWORD, BARE_LABEL) PG_KEYWORD("immutable", IMMUTABLE, UNRESERVED_KEYWORD, BARE_LABEL) PG_KEYWORD("implicit", IMPLICIT_P, UNRESERVED_KEYWORD, BARE_LABEL) +PG_KEYWORD("implies", IMPLIES, UNRESERVED_KEYWORD, BARE_LABEL) PG_KEYWORD("import", IMPORT_P, UNRESERVED_KEYWORD, BARE_LABEL) PG_KEYWORD("in", IN_P, RESERVED_KEYWORD, BARE_LABEL) PG_KEYWORD("include", INCLUDE, UNRESERVED_KEYWORD, BARE_LABEL) diff --git a/src/test/regress/expected/boolean.out b/src/test/regress/expected/boolean.out index 0e99eb7ffc0..caa63f51f40 100644 --- a/src/test/regress/expected/boolean.out +++ b/src/test/regress/expected/boolean.out @@ -566,6 +566,155 @@ SELECT isnul OR istrue OR isfalse FROM booltbl4; t (1 row) +-- Implication: "a IMPLIES b" is "NOT a OR b". It is not commutative, so all +-- nine combinations of three-valued logic have to be checked. +SELECT istrue IMPLIES istrue, istrue IMPLIES isfalse, istrue IMPLIES isnul + FROM booltbl4; + ?column? | ?column? | ?column? +----------+----------+---------- + t | f | (null) +(1 row) + +SELECT isfalse IMPLIES istrue, isfalse IMPLIES isfalse, isfalse IMPLIES isnul + FROM booltbl4; + ?column? | ?column? | ?column? +----------+----------+---------- + t | t | t +(1 row) + +SELECT isnul IMPLIES istrue, isnul IMPLIES isfalse, isnul IMPLIES isnul + FROM booltbl4; + ?column? | ?column? | ?column? +----------+----------+---------- + t | (null) | (null) +(1 row) + +-- the same, as constants, so that constant folding is exercised too +SELECT true IMPLIES true, true IMPLIES false, true IMPLIES null; + ?column? | ?column? | ?column? +----------+----------+---------- + t | f | (null) +(1 row) + +SELECT false IMPLIES true, false IMPLIES false, false IMPLIES null; + ?column? | ?column? | ?column? +----------+----------+---------- + t | t | t +(1 row) + +SELECT null IMPLIES true, null IMPLIES false, null::bool IMPLIES null; + ?column? | ?column? | ?column? +----------+----------+---------- + t | (null) | (null) +(1 row) + +-- IMPLIES is right-associative: false IMPLIES (true IMPLIES false), rather +-- than (false IMPLIES true) IMPLIES false +SELECT isfalse IMPLIES istrue IMPLIES isfalse FROM booltbl4; + ?column? +---------- + t +(1 row) + +-- so a chain is implication from the conjunction of the leading operands +-- (exportation), not implication of their conjunction. The second row is the +-- interesting one: it tells the two apart. +SELECT a, b, c, + a IMPLIES b IMPLIES c AS chained, + (a AND b) IMPLIES c AS conj_antecedent, + a IMPLIES (b AND c) AS conj_consequent + FROM (VALUES (true, true, true), + (true, false, false), + (false, true, false)) AS t(a, b, c); + a | b | c | chained | conj_antecedent | conj_consequent +---+---+---+---------+-----------------+----------------- + t | t | t | t | t | t + t | f | f | t | t | f + f | t | f | t | t | t +(3 rows) + +-- exportation holds for all three truth values, so this returns no rows +SELECT a, b, c + FROM (VALUES (true), (false), (null)) AS x(a), + (VALUES (true), (false), (null)) AS y(b), + (VALUES (true), (false), (null)) AS z(c) + WHERE (a IMPLIES b IMPLIES c) IS DISTINCT FROM ((a AND b) IMPLIES c); + a | b | c +---+---+--- +(0 rows) + +-- and binds looser than OR, AND, NOT, the comparison operators and IS +SELECT istrue OR isfalse IMPLIES isfalse FROM booltbl4; + ?column? +---------- + f +(1 row) + +SELECT isfalse IMPLIES isfalse AND isfalse FROM booltbl4; + ?column? +---------- + t +(1 row) + +SELECT NOT istrue IMPLIES istrue FROM booltbl4; + ?column? +---------- + t +(1 row) + +SELECT 1 = 1 IMPLIES 2 = 3; + ?column? +---------- + f +(1 row) + +SELECT istrue IMPLIES isnul IS NULL FROM booltbl4; + ?column? +---------- + t +(1 row) + +-- non-boolean operands are reported in terms of IMPLIES, not of its expansion +SELECT 1 IMPLIES true; -- error +ERROR: argument of IMPLIES must be type boolean, not type integer +LINE 1: SELECT 1 IMPLIES true; + ^ +SELECT true IMPLIES 1; -- error +ERROR: argument of IMPLIES must be type boolean, not type integer +LINE 1: SELECT true IMPLIES 1; + ^ +-- the construct is expanded during parse analysis, so this is what is stored +CREATE VIEW boolview AS SELECT istrue IMPLIES isnul AS i FROM booltbl4; +SELECT pg_get_viewdef('boolview', true); + pg_get_viewdef +---------------------------------- + SELECT NOT istrue OR isnul AS i+ + FROM booltbl4; +(1 row) + +DROP VIEW boolview; +-- IMPLIES is unreserved, so it remains usable as an identifier +CREATE TABLE implies (implies bool); +INSERT INTO implies VALUES (false); +SELECT implies IMPLIES implies FROM implies; + ?column? +---------- + t +(1 row) + +DROP TABLE implies; +SELECT 1 AS implies; + implies +--------- + 1 +(1 row) + +SELECT 1 implies; + implies +--------- + 1 +(1 row) + -- Casts SELECT 0::boolean; bool diff --git a/src/test/regress/sql/boolean.sql b/src/test/regress/sql/boolean.sql index 85c6b019882..f288cf46726 100644 --- a/src/test/regress/sql/boolean.sql +++ b/src/test/regress/sql/boolean.sql @@ -250,6 +250,66 @@ SELECT isfalse OR isnul OR istrue FROM booltbl4; SELECT istrue OR isfalse OR isnul FROM booltbl4; SELECT isnul OR istrue OR isfalse FROM booltbl4; +-- Implication: "a IMPLIES b" is "NOT a OR b". It is not commutative, so all +-- nine combinations of three-valued logic have to be checked. +SELECT istrue IMPLIES istrue, istrue IMPLIES isfalse, istrue IMPLIES isnul + FROM booltbl4; +SELECT isfalse IMPLIES istrue, isfalse IMPLIES isfalse, isfalse IMPLIES isnul + FROM booltbl4; +SELECT isnul IMPLIES istrue, isnul IMPLIES isfalse, isnul IMPLIES isnul + FROM booltbl4; + +-- the same, as constants, so that constant folding is exercised too +SELECT true IMPLIES true, true IMPLIES false, true IMPLIES null; +SELECT false IMPLIES true, false IMPLIES false, false IMPLIES null; +SELECT null IMPLIES true, null IMPLIES false, null::bool IMPLIES null; + +-- IMPLIES is right-associative: false IMPLIES (true IMPLIES false), rather +-- than (false IMPLIES true) IMPLIES false +SELECT isfalse IMPLIES istrue IMPLIES isfalse FROM booltbl4; + +-- so a chain is implication from the conjunction of the leading operands +-- (exportation), not implication of their conjunction. The second row is the +-- interesting one: it tells the two apart. +SELECT a, b, c, + a IMPLIES b IMPLIES c AS chained, + (a AND b) IMPLIES c AS conj_antecedent, + a IMPLIES (b AND c) AS conj_consequent + FROM (VALUES (true, true, true), + (true, false, false), + (false, true, false)) AS t(a, b, c); + +-- exportation holds for all three truth values, so this returns no rows +SELECT a, b, c + FROM (VALUES (true), (false), (null)) AS x(a), + (VALUES (true), (false), (null)) AS y(b), + (VALUES (true), (false), (null)) AS z(c) + WHERE (a IMPLIES b IMPLIES c) IS DISTINCT FROM ((a AND b) IMPLIES c); + +-- and binds looser than OR, AND, NOT, the comparison operators and IS +SELECT istrue OR isfalse IMPLIES isfalse FROM booltbl4; +SELECT isfalse IMPLIES isfalse AND isfalse FROM booltbl4; +SELECT NOT istrue IMPLIES istrue FROM booltbl4; +SELECT 1 = 1 IMPLIES 2 = 3; +SELECT istrue IMPLIES isnul IS NULL FROM booltbl4; + +-- non-boolean operands are reported in terms of IMPLIES, not of its expansion +SELECT 1 IMPLIES true; -- error +SELECT true IMPLIES 1; -- error + +-- the construct is expanded during parse analysis, so this is what is stored +CREATE VIEW boolview AS SELECT istrue IMPLIES isnul AS i FROM booltbl4; +SELECT pg_get_viewdef('boolview', true); +DROP VIEW boolview; + +-- IMPLIES is unreserved, so it remains usable as an identifier +CREATE TABLE implies (implies bool); +INSERT INTO implies VALUES (false); +SELECT implies IMPLIES implies FROM implies; +DROP TABLE implies; +SELECT 1 AS implies; +SELECT 1 implies; + -- Casts SELECT 0::boolean; SELECT 1::boolean; -- 2.55.0