Tuple Relational Calculus - Learning Module

Loading content...

0/241

Complex Formulas

Unleashing the Full Power of TRC

We have now covered all the components of Tuple Relational Calculus: tuple variables that range over relations, range expressions that bind them, and atomic formulas that express primitive conditions. But the true expressive power of TRC emerges when we compose these elements into complex formulas.

Complex formulas combine atoms using logical connectives (¬, ∧, ∨, →) and quantifiers (∃, ∀) to express queries that would require multiple operations in relational algebra. A single complex formula can encode selections, projections, joins, set operations, and even division—all through the elegant language of predicate logic.

This page explores the art and science of constructing complex formulas:

How to methodically build formulas for specific query requirements
Nested quantification patterns and their meanings
Equivalence between TRC formulas and relational algebra expressions
Advanced query patterns that showcase TRC's declarative elegance
Practical translation to SQL subqueries

What You Will Learn

By the end of this page, you will master the construction of arbitrarily complex TRC formulas, understand nested quantification, recognize the correspondence with relational algebra, and be able to express sophisticated queries with logical precision.

Building Formulas with Logical Connectives

Logical connectives are the mortar that binds atomic formulas into complex structures. Each connective serves distinct purposes in query construction.

Conjunction (∧) — The AND Connective:

Conjunction is the most fundamental combiner. It expresses that all conditions must hold simultaneously.

Uses:

Multiple selection criteria: e.salary > 50000 ∧ e.age < 40
Join conditions: Employee(e) ∧ Department(d) ∧ e.dept_id = d.dept_id
Combining range with filters: R(t) ∧ atom₁ ∧ atom₂ ∧ ...

Properties:

Commutative: P ∧ Q ≡ Q ∧ P
Associative: (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R)
Identity: P ∧ TRUE ≡ P
Annihilator: P ∧ FALSE ≡ FALSE

Disjunction (∨) — The OR Connective:

Disjunction expresses alternatives—at least one condition must hold.

Uses:

Alternative values: e.dept_id = 5 ∨ e.dept_id = 7
Flexible matching: e.title = 'Manager' ∨ e.salary > 100000
Safety with universals: In some constructions

Properties:

Commutative: P ∨ Q ≡ Q ∨ P
Associative: (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R)
Identity: P ∨ FALSE ≡ P
Annihilator: P ∨ TRUE ≡ TRUE

Disjunction and Safety

Disjunction can cause safety problems if one branch lacks a positive range. For example, R(t) ∨ t.A > 5 is unsafe—the second branch doesn't constrain t to a relation. Always ensure all disjuncts properly bound tuple variables.

Negation (¬) — The NOT Connective:

Negation inverts truth values, enabling exclusion conditions.

Uses:

Simple exclusion: ¬(e.status = 'Inactive')
Non-existence: ¬∃t(R(t) ∧ condition) — "no such tuple exists"
Universal via negation: ∀t(P) ≡ ¬∃t(¬P)

Caution: Negation on free variables can cause safety issues:

✗ { t | ¬Employee(t) }  -- Infinite result!
✓ { e | Employee(e) ∧ ¬∃d(Department(d) ∧ e.dept_id = d.dept_id) }  -- Safe

Implication (→) — The IF-THEN Connective:

Implication expresses conditional statements, crucial for universal quantification.

Uses:

Restricted universals: ∀t(R(t) → condition)
Integrity constraints: e.age ≥ 18 → e.can_work = TRUE

Key Equivalence:

P → Q ≡ ¬P ∨ Q

This allows rewriting implications without the → operator if needed.

connective-examples.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
-- CONJUNCTION: Multiple criteria on same tuple
{ e | Employee(e) ∧ 
      e.salary > 50000 ∧ 
      e.dept_id = 5 ∧ 
      e.hire_date > DATE '2020-01-01' }
 
-- DISJUNCTION: Alternative conditions
{ e | Employee(e) ∧ (e.dept_id = 5 ∨ e.dept_id = 7 ∨ e.title = 'Executive') }
 
-- NEGATION: Exclusion
{ e | Employee(e) ∧ ¬(e.status = 'Terminated') ∧ ¬(e.dept_id = 99) }
 
-- COMBINED: Complex business logic
{ e | Employee(e) ∧ 
      ((e.salary > 100000 ∧ e.tenure > 5) ∨ 
       (e.title = 'Director' ∧ e.performance = 'Excellent')) ∧
      ¬(e.on_leave = TRUE) }
 
-- IMPLICATION in universal (find depts where all earn > 50K)
{ d | Department(d) ∧ 
      ∀e(Employee(e) ∧ e.dept_id = d.dept_id → e.salary > 50000) }

Nested Quantification

Nested quantifiers allow formulas to express multi-level dependencies and relationships. Understanding nesting is key to advanced TRC queries.

Nesting Patterns:

Pattern 1: ∃∃ (Exists-Exists)

Find tuples where multiple related tuples exist:

{ e | Employee(e) ∧ 
      ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.budget > 1000000) ∧
      ∃p(Project(p) ∧ p.lead_id = e.emp_id) }

Employees who work in high-budget departments AND lead a project.

Pattern 2: ∃∀ (Exists-ForAll)

Find tuples where there exists something satisfying a universal property:

{ d | Department(d) ∧ 
      ∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧
         ∀p(Project(p) ∧ p.dept_id = d.dept_id → 
            ∃a(Assignment(a) ∧ a.emp_id = e.emp_id ∧ a.proj_id = p.proj_id))) }

Departments where at least one employee works on ALL department projects.

Quantifier Nesting Patterns
Pattern	English Meaning	Use Case
`∃x∃y(P(x,y))`	Some x and some y satisfy P	Multiple related tuples exist
`∃x∀y(P(x,y))`	Some x relates properly to all y	Universal consumer exists
`∀x∃y(P(x,y))`	For each x, some y relates	Each has at least one match
`∀x∀y(P(x,y))`	All pairs satisfy P	Complete relationship

Pattern 3: ∀∃ (ForAll-Exists)

For every tuple of one kind, there exists a related tuple:

{ c | Customer(c) ∧ 
      ∀p(Product(p) → 
         ∃o(Order(o) ∧ o.customer_id = c.cust_id ∧ o.product_id = p.prod_id)) }

Customers who have ordered every product.

Pattern 4: ∀∀ (ForAll-ForAll)

All pairs must satisfy a condition:

{ m | Manager(m) ∧ 
      ∀e₁∀e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.manager = m.id ∧ e₂.manager = m.id ∧ e₁ ≠ e₂ →
              |e₁.salary - e₂.salary| < 10000) }

Managers whose direct reports all have similar salaries (within 10K of each other).

Order Matters

The order of quantifiers changes meaning dramatically. '∃x∀y P(x,y)' means 'there is one x that works for all y'. '∀y∃x P(x,y)' means 'for each y, there's some x (possibly different)'. When constructing nested quantifiers, be precise about which relationship you mean.

nested-quantifiers.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
-- DIVISION QUERY: Students enrolled in ALL required courses
-- This is the classic "for all" pattern
 
{ s | Student(s) ∧ 
      ∀c(RequiredCourse(c) → 
         ∃e(Enrollment(e) ∧ e.student_id = s.id ∧ e.course_id = c.id)) }
 
-- Breaking it down:
-- For student s to be in the result:
--   For every required course c:
--     There must exist an enrollment e linking s to c
 
-- EMPLOYEES WHO MANAGE SOMEONE WHO MANAGES SOMEONE
-- Triple-nested existential
 
{ e | Employee(e) ∧ 
      ∃m(Employee(m) ∧ m.manager_id = e.emp_id ∧
         ∃s(Employee(s) ∧ s.manager_id = m.emp_id)) }
 
-- PRODUCTS ORDERED BY ALL PREMIUM CUSTOMERS
-- Nested ∀∃
 
{ p | Product(p) ∧ 
      ∀c(Customer(c) ∧ c.tier = 'Premium' → 
         ∃o(Order(o) ∧ o.customer_id = c.id ∧ o.product_id = p.id)) }

TRC and Relational Algebra Correspondence

TRC and relational algebra are equivalent in expressive power—anything one can express, the other can express (within certain bounds). Understanding this correspondence deepens comprehension of both.

Selection (σ):

Algebra: σ_{condition}(R)
TRC:     { t | R(t) ∧ condition }

The selection condition becomes a conjunction with the range predicate.

Projection (π):

Algebra: π_{A,B}(R)
TRC:     { t.A, t.B | R(t) }

The target list specifies the projected attributes.

Cartesian Product (×):

Algebra: R × S
TRC:     { t, s | R(t) ∧ S(s) }

Multiple free variables with separate range predicates.

Join (⋈):

Algebra: R ⋈_{condition} S
TRC:     { t, s | R(t) ∧ S(s) ∧ condition }

Cartesian product filtered by the join condition.

Relational Algebra to TRC Translation
Algebra	TRC Equivalent
`σ_P(R)`	`{ t \| R(t) ∧ P }`
`π_{A,B}(R)`	`{ t.A, t.B \| R(t) }`
`R × S`	`{ t, s \| R(t) ∧ S(s) }`
`R ⋈_C S`	`{ t, s \| R(t) ∧ S(s) ∧ C }`
`R ∪ S`	`{ t \| R(t) ∨ S(t) }`
`R - S`	`{ t \| R(t) ∧ ¬S(t) }`
`R ∩ S`	`{ t \| R(t) ∧ S(t) }`
`R ÷ S`	`{ t \| ... ∀s(S(s) → ∃r(...)) }`

Union (∪):

Algebra: R ∪ S  (R and S must be union-compatible)
TRC:     { t | R(t) ∨ S(t) }

Disjunction with the same tuple variable ranging over both.

Set Difference (−):

Algebra: R − S
TRC:     { t | R(t) ∧ ¬S(t) }

Tuples in R but not in S.

Intersection (∩):

Algebra: R ∩ S
TRC:     { t | R(t) ∧ S(t) }

Tuples that must be in both relations.

Division (÷):

The most complex operation, naturally expressed in TRC:

Algebra: R(A,B) ÷ S(B)

TRC:     { t.A | R(t) ∧ ∀s(S(s) → ∃r(R(r) ∧ r.A = t.A ∧ r.B = s.B)) }

For each A value in R, check if it pairs with EVERY B value in S.

Codd's Theorem

Codd's theorem states that safe TRC and relational algebra are equivalent in expressive power. This means any query expressible in one can be translated to the other—they define the same class of computable queries, which we call 'relationally complete' queries.

Advanced Query Patterns

Complex formulas enable sophisticated query patterns that appear frequently in real-world data analysis.

Pattern 1: Division (Universal Requirement)

Find entities that satisfy a relationship with ALL members of a set:

"Find suppliers who supply ALL red parts."

{ s | Supplier(s) ∧ 
      ∀p(Part(p) ∧ p.color = 'Red' → 
         ∃sp(Supply(sp) ∧ sp.supplier_id = s.id ∧ sp.part_id = p.id)) }

Pattern 2: Maximum/Minimum (Without Aggregates)

Pure TRC lacks aggregates, but comparisons can find extremes:

"Find the highest paid employee(s)."

{ e | Employee(e) ∧ 
      ¬∃e₂(Employee(e₂) ∧ e₂.salary > e.salary) }

No one earns more than e.

Pattern 3: Exactly N (Counting Without COUNT)

"Find departments with exactly 2 employees."

{ d | Department(d) ∧ 
      ∃e₁∃e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.dept_id = d.dept_id ∧ e₂.dept_id = d.dept_id ∧ 
              e₁.emp_id ≠ e₂.emp_id ∧
              ¬∃e₃(Employee(e₃) ∧ e₃.dept_id = d.dept_id ∧ 
                   e₃.emp_id ≠ e₁.emp_id ∧ e₃.emp_id ≠ e₂.emp_id)) }

Two distinct employees exist, and no third exists.

Transitive Closure AttemptFinding all ancestors (limited depth)

Input

Goal: Find all managers above an employee (any level)

TRC can express fixed depth:
{ m | Employee(m) ∧ 
      (e.manager_id = m.emp_id ∨  -- Direct manager
       ∃m₁(e.manager_id = m₁.emp_id ∧ m₁.manager_id = m.emp_id) ∨  -- 2 levels
       ∃m₁∃m₂(...)) }  -- 3 levels, etc.

Output

For bounded depth: expressible. For unbounded depth: not expressible in pure TRC.

Explanation

TRC (and basic relational algebra) cannot express unbounded transitive closure. Each level requires explicit quantification. This limitation is why SQL added recursive CTEs.

advanced-patterns.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
-- ANTI-JOIN: Employees with no assignments
{ e | Employee(e) ∧ ¬∃a(Assignment(a) ∧ a.emp_id = e.emp_id) }
 
-- SEMI-JOIN: Departments that have at least one high earner
{ d | Department(d) ∧ ∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ e.salary > 100000) }
 
-- SECOND HIGHEST (without aggregates):
-- Find employees earning less than max, but more than all others below max
{ e | Employee(e) ∧ 
      ∃top(Employee(top) ∧ top.salary > e.salary ∧ 
           ¬∃above(Employee(above) ∧ above.salary > top.salary)) ∧
      ¬∃between(Employee(between) ∧ between.salary > e.salary ∧ 
                ∃top2(Employee(top2) ∧ top2.salary > between.salary ∧
                     ¬∃above2(Employee(above2) ∧ above2.salary > top2.salary))) }
 
-- Actually simpler: second highest = maximum of those below maximum
{ e | Employee(e) ∧ 
      ∃top(Employee(top) ∧ ¬∃t2(Employee(t2) ∧ t2.salary > top.salary) ∧ 
           top.salary > e.salary) ∧
      ¬∃e2(Employee(e2) ∧ e2.salary > e.salary ∧ 
           ∃top(Employee(top) ∧ ¬∃t2(Employee(t2) ∧ t2.salary > top.salary) ∧ 
                top.salary > e2.salary)) }

Pattern Library

Build a personal library of complex formula patterns. When facing a new query requirement, first check if it matches a known pattern. Division, maximum, counting, and set comparisons are the most common patterns you'll encounter.

Formula Transformation and Optimization

Complex formulas can often be rewritten into equivalent forms that are easier to understand, optimize, or execute.

De Morgan's Laws:

¬(P ∧ Q) ≡ ¬P ∨ ¬Q
¬(P ∨ Q) ≡ ¬P ∧ ¬Q

Quantifier Duality:

¬∃t(P(t)) ≡ ∀t(¬P(t))
¬∀t(P(t)) ≡ ∃t(¬P(t))

These allow converting between existential and universal forms.

Pushing Negation Inward:

¬∃e(Employee(e) ∧ e.salary > 100000)
≡ ∀e(¬(Employee(e) ∧ e.salary > 100000))
≡ ∀e(¬Employee(e) ∨ e.salary ≤ 100000)
≡ ∀e(Employee(e) → e.salary ≤ 100000)

"No employee earns more than 100K" becomes "All employees earn ≤100K."

Converting Universal to Negated Existential:

This is the most practical transformation for SQL:

∀t(R(t) → P(t))
≡ ¬∃t(R(t) ∧ ¬P(t))

"All R satisfy P" becomes "No R violates P." SQL implements this as NOT EXISTS.

Key Formula Equivalences
Original	Equivalent	Use Case
`∀t(R(t) → P(t))`	`¬∃t(R(t) ∧ ¬P(t))`	Universal to NOT EXISTS
`¬(P ∧ Q)`	`¬P ∨ ¬Q`	Negation distribution
`P → Q`	`¬P ∨ Q`	Implication elimination
`∃t(P(t)) ∧ ∃t(Q(t))`	`∃t(P(t)) ∧ ∃s(Q(s))`	Scope clarification
`∀t∀s(P(t,s))`	`∀s∀t(P(t,s))`	Quantifier reordering (same type)

formula-transformation.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- ORIGINAL: Departments where all employees earn > 50000
{ d | Department(d) ∧ ∀e(Employee(e) ∧ e.dept_id = d.dept_id → e.salary > 50000) }
 
-- STEP 1: Apply implication equivalence
-- ∀e(¬(Employee(e) ∧ e.dept_id = d.dept_id) ∨ e.salary > 50000)
 
-- STEP 2: Apply quantifier duality
{ d | Department(d) ∧ ¬∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ ¬(e.salary > 50000)) }
 
-- STEP 3: Simplify inner negation
{ d | Department(d) ∧ ¬∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ e.salary ≤ 50000) }
 
-- This form translates directly to SQL NOT EXISTS:
-- SELECT d.* FROM Department d
-- WHERE NOT EXISTS (
--     SELECT 1 FROM Employee e
--     WHERE e.dept_id = d.dept_id AND e.salary <= 50000
-- )

Optimization Insight

The negated existential form is often more efficient to execute than a universal check. Finding one counterexample (in NOT EXISTS) can short-circuit, while verifying all (in a true FORALL) must examine everything. Query optimizers exploit this.

SQL Translation of Complex Formulas

Translating complex TRC formulas to SQL requires mapping each construct to its SQL equivalent. This section provides systematic translation patterns.

Existential Subqueries:

∃t(R(t) ∧ condition)  →  EXISTS (SELECT 1 FROM R t WHERE condition)

Universal Subqueries:

∀t(R(t) → condition)  →  NOT EXISTS (SELECT 1 FROM R t WHERE NOT condition)

Nested Quantifiers:

Each quantifier becomes a subquery, nested correspondingly.

complex-to-sql.sql

-- TRC: Find customers who have ordered ALL products
-- { c | Customer(c) ∧ ∀p(Product(p) → ∃o(Order(o) ∧ o.cust_id = c.id ∧ o.prod_id = p.id)) }
 
-- SQL Translation:
SELECT c.*
FROM Customer c
WHERE NOT EXISTS (  -- ∀p translates to NOT EXISTS (... NOT ...)
    SELECT 1 
    FROM Product p
    WHERE NOT EXISTS (  -- ¬∃o becomes NOT EXISTS
        SELECT 1 
        FROM Order o
        WHERE o.cust_id = c.id 
          AND o.prod_id = p.id
    )
);
 
-- TRC: Find employees earning more than everyone in Sales
-- { e | Employee(e) ∧ ∀s(Employee(s) ∧ s.dept_id = 'Sales' → e.salary > s.salary) }
 
-- SQL Translation:
SELECT e.*
FROM Employee e
WHERE NOT EXISTS (
    SELECT 1 
    FROM Employee s
    WHERE s.dept_id = 'Sales' 
      AND NOT (e.salary > s.salary)  -- e.salary <= s.salary
);
 
-- Alternative using ALL (SQL extension):
SELECT e.*
FROM Employee e
WHERE e.salary > ALL (
    SELECT s.salary FROM Employee s WHERE s.dept_id = 'Sales'
);

Correlated Subqueries:

In the translations above, inner subqueries reference outer tuple variables (c.id, e.salary). These are correlated subqueries—they execute once per outer tuple, using outer values as parameters.

This is precisely the bound-free variable relationship in TRC: inner quantified variables can reference outer free variables.

Multiple EXISTS:

Conjunctions of existentials become multiple EXISTS clauses:

TRC: ∃d(D(d) ∧ P(d)) ∧ ∃p(P(p) ∧ Q(p))
SQL: EXISTS (... D ...) AND EXISTS (... P ...)

Disjunction of EXISTS:

TRC: ∃d(D(d) ∧ P(d)) ∨ ∃p(P(p) ∧ Q(p))
SQL: EXISTS (...) OR EXISTS (...)

The NOT EXISTS Double Negation

Universal quantification in SQL always involves double NOT: NOT EXISTS (... WHERE NOT condition). This pattern might seem awkward, but it's the direct translation of '∀x(P(x) → Q(x))' to '¬∃x(P(x) ∧ ¬Q(x))'. Recognize this pattern and you can express any universal constraint.

Common Pitfalls and Debugging

Complex formulas are prone to subtle errors. Understanding common pitfalls prevents frustration.

Pitfall 1: Incorrect Quantifier Order

✗ "Some employee manages all projects"
  ∀p(Project(p) → ∃e(Employee(e) ∧ manages(e, p)))
  -- This says: Each project has SOME manager (possibly different)

✓ "Some employee manages all projects"
  ∃e(Employee(e) ∧ ∀p(Project(p) → manages(e, p)))
  -- This correctly says: ONE employee manages ALL projects

Pitfall 2: Missing Range Predicates

✗ { e | e.salary > 50000 ∧ ∃d(e.dept_id = d.dept_id ∧ d.budget > 1000000) }
  -- e has no range predicate! d has no range predicate!

✓ { e | Employee(e) ∧ e.salary > 50000 ∧ 
        ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.budget > 1000000) }

Pitfall 3: Variable Scope Confusion

✗ { e | Employee(e) ∧ (∃d(Department(d) ∧ e.dept_id = d.dept_id)) ∧ d.name = 'HR' }
  -- d is out of scope after the existential closes!

✓ { e | Employee(e) ∧ ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.name = 'HR') }
  -- All d references inside the existential scope

Debugging Checklist

•Range Check: Does every tuple variable have a positive range predicate (R(t))?
•Scope Check: Are all variable references within their quantifier's scope?
•Quantifier Order: Does the nesting match the intended reading (left-to-right)?
•Implication in Universals: Does ∀ use the pattern ∀t(R(t) → condition)?
•Target Variables: Are all variables in the target list free in the formula?
•Type Compatibility: Do all comparisons involve compatible types?
•NULL Handling: Could NULLs cause unexpected UNKNOWN results?

Debugging Strategy:

Start Simple: Write the simplest version of the query first
Test Components: Test subformulas independently
Add Complexity Gradually: Add one condition at a time, verifying each
Check Edge Cases: What if the quantified set is empty?
- ∃t(P(t)) over empty set → FALSE
- ∀t(P(t)) over empty set → TRUE (vacuously true)
Trace Evaluation: Manually evaluate with small sample data

Vacuous Truth

∀t(P(t)) is TRUE when no t exists to check! This catches beginners: '∀e(... → e.salary > 50000)' for a department with NO employees returns TRUE (department is included). Consider whether this behavior matches your intent.

Real-World Complex Query Examples

Let's conclude with comprehensive real-world examples demonstrating the full power of complex TRC formulas.

Example 1: Supplier with Complete Red Parts Coverage

Business Need: Find suppliers who can supply all red parts in our catalog.

real-world-example-1.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
-- Schema:
-- Supplier(supplier_id, name, location)
-- Part(part_id, name, color)
-- Catalog(supplier_id, part_id, price)
 
-- TRC Query:
{ s | Supplier(s) ∧ 
      ∀p(Part(p) ∧ p.color = 'Red' → 
         ∃c(Catalog(c) ∧ c.supplier_id = s.supplier_id ∧ c.part_id = p.part_id)) }
 
-- English: A supplier s is in the result if and only if
--          for every red part p, there exists a catalog entry c
--          linking s to p.
 
-- SQL Translation:
SELECT s.*
FROM Supplier s
WHERE NOT EXISTS (
    SELECT 1 FROM Part p
    WHERE p.color = 'Red'
      AND NOT EXISTS (
          SELECT 1 FROM Catalog c
          WHERE c.supplier_id = s.supplier_id
            AND c.part_id = p.part_id
      )
);

Example 2: Employees Outearning Their Entire Management Chain

Business Need: Find employees who earn more than both their direct manager AND their manager's manager.

real-world-example-2.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
-- Schema:
-- Employee(emp_id, name, salary, manager_id)
 
-- TRC Query:
{ e | Employee(e) ∧ 
      ∃m(Employee(m) ∧ e.manager_id = m.emp_id ∧ e.salary > m.salary ∧
         ∃mm(Employee(mm) ∧ m.manager_id = mm.emp_id ∧ e.salary > mm.salary)) }
 
-- English: Employee e earns more than their manager m,
--          and m has a manager mm, and e earns more than mm too.
 
-- Note: This only considers 2 levels. For arbitrary depth, 
--       recursive constructs (not standard TRC) would be needed.
 
-- SQL Translation:
SELECT e.*
FROM Employee e
WHERE EXISTS (
    SELECT 1 FROM Employee m
    WHERE e.manager_id = m.emp_id
      AND e.salary > m.salary
      AND EXISTS (
          SELECT 1 FROM Employee mm
          WHERE m.manager_id = mm.emp_id
            AND e.salary > mm.salary
      )
);

Example 3: Departments with Balanced Teams

Business Need: Find departments where no employee earns more than double another employee's salary.

real-world-example-3.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- TRC Query:
{ d | Department(d) ∧ 
      ∀e₁∀e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.dept_id = d.dept_id ∧ e₂.dept_id = d.dept_id →
              e₁.salary ≤ 2 * e₂.salary) }
 
-- English: For all pairs of employees in department d,
--          neither earns more than double the other.
 
-- SQL Translation (using double NOT EXISTS):
SELECT d.*
FROM Department d
WHERE NOT EXISTS (
    SELECT 1 FROM Employee e1, Employee e2
    WHERE e1.dept_id = d.dept_id
      AND e2.dept_id = d.dept_id
      AND e1.salary > 2 * e2.salary  -- Violation of balance
);

Summary: Mastering Complex Formulas

Key Takeaways

•Connective Mastery: ∧ (and), ∨ (or), ¬ (not), → (implies) combine atoms into complex conditions with precise semantics
•Nested Quantification: ∃∃, ∃∀, ∀∃, ∀∀ patterns express multi-level relationships; quantifier order matters critically
•TRC-Algebra Equivalence: Each relational algebra operation has a TRC equivalent; they are expressively equal (Codd's theorem)
•Advanced Patterns: Division, maximum finding, counting, and set comparisons follow recognizable complex formula templates
•Formula Transformation: De Morgan's laws, quantifier duality, and implication elimination enable query optimization
•SQL Translation: EXISTS implements ∃; NOT EXISTS with inner NOT implements ∀; nested quantifiers become nested subqueries
•Debugging Discipline: Check range predicates, variable scope, quantifier order, and handle edge cases (empty sets, NULLs)

Module Complete!

You have now completed the comprehensive study of Tuple Relational Calculus. From tuple variables and range expressions, through formula syntax and atomic formulas, to the complex formulas covered here—you now possess a rigorous understanding of this foundational query formalism.

This knowledge empowers you to:

Read and write formal database specifications
Understand SQL at its logical foundations
Reason about query equivalence and optimization
Recognize the declarative vs. procedural distinction
Prepare for advanced topics like Domain Relational Calculus and query optimization theory

Module Complete

Congratulations! You have mastered Tuple Relational Calculus—from its fundamental building blocks to its most sophisticated expressions. You can now express arbitrarily complex database queries using the elegant language of predicate logic, and translate between TRC and SQL with precision.

Complex Formulas

Unleashing the Full Power of TRC

This page explores the art and science of constructing complex formulas:

How to methodically build formulas for specific query requirements
Nested quantification patterns and their meanings
Equivalence between TRC formulas and relational algebra expressions
Advanced query patterns that showcase TRC's declarative elegance
Practical translation to SQL subqueries

What You Will Learn

Building Formulas with Logical Connectives

Logical connectives are the mortar that binds atomic formulas into complex structures. Each connective serves distinct purposes in query construction.

Conjunction (∧) — The AND Connective:

Conjunction is the most fundamental combiner. It expresses that all conditions must hold simultaneously.

Uses:

Multiple selection criteria: e.salary > 50000 ∧ e.age < 40
Join conditions: Employee(e) ∧ Department(d) ∧ e.dept_id = d.dept_id
Combining range with filters: R(t) ∧ atom₁ ∧ atom₂ ∧ ...

Properties:

Commutative: P ∧ Q ≡ Q ∧ P
Associative: (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R)
Identity: P ∧ TRUE ≡ P
Annihilator: P ∧ FALSE ≡ FALSE

Disjunction (∨) — The OR Connective:

Disjunction expresses alternatives—at least one condition must hold.

Uses:

Alternative values: e.dept_id = 5 ∨ e.dept_id = 7
Flexible matching: e.title = 'Manager' ∨ e.salary > 100000
Safety with universals: In some constructions

Properties:

Commutative: P ∨ Q ≡ Q ∨ P
Associative: (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R)
Identity: P ∨ FALSE ≡ P
Annihilator: P ∨ TRUE ≡ TRUE

Disjunction and Safety

Negation (¬) — The NOT Connective:

Negation inverts truth values, enabling exclusion conditions.

Uses:

Simple exclusion: ¬(e.status = 'Inactive')
Non-existence: ¬∃t(R(t) ∧ condition) — "no such tuple exists"
Universal via negation: ∀t(P) ≡ ¬∃t(¬P)

Caution: Negation on free variables can cause safety issues:

✗ { t | ¬Employee(t) }  -- Infinite result!
✓ { e | Employee(e) ∧ ¬∃d(Department(d) ∧ e.dept_id = d.dept_id) }  -- Safe

Implication (→) — The IF-THEN Connective:

Implication expresses conditional statements, crucial for universal quantification.

Uses:

Restricted universals: ∀t(R(t) → condition)
Integrity constraints: e.age ≥ 18 → e.can_work = TRUE

Key Equivalence:

P → Q ≡ ¬P ∨ Q

This allows rewriting implications without the → operator if needed.

connective-examples.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
-- CONJUNCTION: Multiple criteria on same tuple
{ e | Employee(e) ∧ 
      e.salary > 50000 ∧ 
      e.dept_id = 5 ∧ 
      e.hire_date > DATE '2020-01-01' }
 
-- DISJUNCTION: Alternative conditions
{ e | Employee(e) ∧ (e.dept_id = 5 ∨ e.dept_id = 7 ∨ e.title = 'Executive') }
 
-- NEGATION: Exclusion
{ e | Employee(e) ∧ ¬(e.status = 'Terminated') ∧ ¬(e.dept_id = 99) }
 
-- COMBINED: Complex business logic
{ e | Employee(e) ∧ 
      ((e.salary > 100000 ∧ e.tenure > 5) ∨ 
       (e.title = 'Director' ∧ e.performance = 'Excellent')) ∧
      ¬(e.on_leave = TRUE) }
 
-- IMPLICATION in universal (find depts where all earn > 50K)
{ d | Department(d) ∧ 
      ∀e(Employee(e) ∧ e.dept_id = d.dept_id → e.salary > 50000) }

Nested Quantification

Nested quantifiers allow formulas to express multi-level dependencies and relationships. Understanding nesting is key to advanced TRC queries.

Nesting Patterns:

Pattern 1: ∃∃ (Exists-Exists)

Find tuples where multiple related tuples exist:

{ e | Employee(e) ∧ 
      ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.budget > 1000000) ∧
      ∃p(Project(p) ∧ p.lead_id = e.emp_id) }

Employees who work in high-budget departments AND lead a project.

Pattern 2: ∃∀ (Exists-ForAll)

Find tuples where there exists something satisfying a universal property:

{ d | Department(d) ∧ 
      ∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧
         ∀p(Project(p) ∧ p.dept_id = d.dept_id → 
            ∃a(Assignment(a) ∧ a.emp_id = e.emp_id ∧ a.proj_id = p.proj_id))) }

Departments where at least one employee works on ALL department projects.

Quantifier Nesting Patterns
Pattern	English Meaning	Use Case
`∃x∃y(P(x,y))`	Some x and some y satisfy P	Multiple related tuples exist
`∃x∀y(P(x,y))`	Some x relates properly to all y	Universal consumer exists
`∀x∃y(P(x,y))`	For each x, some y relates	Each has at least one match
`∀x∀y(P(x,y))`	All pairs satisfy P	Complete relationship

Pattern 3: ∀∃ (ForAll-Exists)

For every tuple of one kind, there exists a related tuple:

{ c | Customer(c) ∧ 
      ∀p(Product(p) → 
         ∃o(Order(o) ∧ o.customer_id = c.cust_id ∧ o.product_id = p.prod_id)) }

Customers who have ordered every product.

Pattern 4: ∀∀ (ForAll-ForAll)

All pairs must satisfy a condition:

{ m | Manager(m) ∧ 
      ∀e₁∀e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.manager = m.id ∧ e₂.manager = m.id ∧ e₁ ≠ e₂ →
              |e₁.salary - e₂.salary| < 10000) }

Managers whose direct reports all have similar salaries (within 10K of each other).

Order Matters

nested-quantifiers.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
-- DIVISION QUERY: Students enrolled in ALL required courses
-- This is the classic "for all" pattern
 
{ s | Student(s) ∧ 
      ∀c(RequiredCourse(c) → 
         ∃e(Enrollment(e) ∧ e.student_id = s.id ∧ e.course_id = c.id)) }
 
-- Breaking it down:
-- For student s to be in the result:
--   For every required course c:
--     There must exist an enrollment e linking s to c
 
-- EMPLOYEES WHO MANAGE SOMEONE WHO MANAGES SOMEONE
-- Triple-nested existential
 
{ e | Employee(e) ∧ 
      ∃m(Employee(m) ∧ m.manager_id = e.emp_id ∧
         ∃s(Employee(s) ∧ s.manager_id = m.emp_id)) }
 
-- PRODUCTS ORDERED BY ALL PREMIUM CUSTOMERS
-- Nested ∀∃
 
{ p | Product(p) ∧ 
      ∀c(Customer(c) ∧ c.tier = 'Premium' → 
         ∃o(Order(o) ∧ o.customer_id = c.id ∧ o.product_id = p.id)) }

TRC and Relational Algebra Correspondence

Selection (σ):

Algebra: σ_{condition}(R)
TRC:     { t | R(t) ∧ condition }

The selection condition becomes a conjunction with the range predicate.

Projection (π):

Algebra: π_{A,B}(R)
TRC:     { t.A, t.B | R(t) }

The target list specifies the projected attributes.

Cartesian Product (×):

Algebra: R × S
TRC:     { t, s | R(t) ∧ S(s) }

Multiple free variables with separate range predicates.

Join (⋈):

Algebra: R ⋈_{condition} S
TRC:     { t, s | R(t) ∧ S(s) ∧ condition }

Cartesian product filtered by the join condition.

Relational Algebra to TRC Translation
Algebra	TRC Equivalent
`σ_P(R)`	`{ t \| R(t) ∧ P }`
`π_{A,B}(R)`	`{ t.A, t.B \| R(t) }`
`R × S`	`{ t, s \| R(t) ∧ S(s) }`
`R ⋈_C S`	`{ t, s \| R(t) ∧ S(s) ∧ C }`
`R ∪ S`	`{ t \| R(t) ∨ S(t) }`
`R - S`	`{ t \| R(t) ∧ ¬S(t) }`
`R ∩ S`	`{ t \| R(t) ∧ S(t) }`
`R ÷ S`	`{ t \| ... ∀s(S(s) → ∃r(...)) }`

Union (∪):

Algebra: R ∪ S  (R and S must be union-compatible)
TRC:     { t | R(t) ∨ S(t) }

Disjunction with the same tuple variable ranging over both.

Set Difference (−):

Algebra: R − S
TRC:     { t | R(t) ∧ ¬S(t) }

Tuples in R but not in S.

Intersection (∩):

Algebra: R ∩ S
TRC:     { t | R(t) ∧ S(t) }

Tuples that must be in both relations.

Division (÷):

The most complex operation, naturally expressed in TRC:

Algebra: R(A,B) ÷ S(B)

TRC:     { t.A | R(t) ∧ ∀s(S(s) → ∃r(R(r) ∧ r.A = t.A ∧ r.B = s.B)) }

For each A value in R, check if it pairs with EVERY B value in S.

Codd's Theorem

Advanced Query Patterns

Complex formulas enable sophisticated query patterns that appear frequently in real-world data analysis.

Pattern 1: Division (Universal Requirement)

Find entities that satisfy a relationship with ALL members of a set:

"Find suppliers who supply ALL red parts."

{ s | Supplier(s) ∧ 
      ∀p(Part(p) ∧ p.color = 'Red' → 
         ∃sp(Supply(sp) ∧ sp.supplier_id = s.id ∧ sp.part_id = p.id)) }

Pattern 2: Maximum/Minimum (Without Aggregates)

Pure TRC lacks aggregates, but comparisons can find extremes:

"Find the highest paid employee(s)."

{ e | Employee(e) ∧ 
      ¬∃e₂(Employee(e₂) ∧ e₂.salary > e.salary) }

No one earns more than e.

Pattern 3: Exactly N (Counting Without COUNT)

"Find departments with exactly 2 employees."

{ d | Department(d) ∧ 
      ∃e₁∃e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.dept_id = d.dept_id ∧ e₂.dept_id = d.dept_id ∧ 
              e₁.emp_id ≠ e₂.emp_id ∧
              ¬∃e₃(Employee(e₃) ∧ e₃.dept_id = d.dept_id ∧ 
                   e₃.emp_id ≠ e₁.emp_id ∧ e₃.emp_id ≠ e₂.emp_id)) }

Two distinct employees exist, and no third exists.

Transitive Closure AttemptFinding all ancestors (limited depth)

Input

Goal: Find all managers above an employee (any level)

TRC can express fixed depth:
{ m | Employee(m) ∧ 
      (e.manager_id = m.emp_id ∨  -- Direct manager
       ∃m₁(e.manager_id = m₁.emp_id ∧ m₁.manager_id = m.emp_id) ∨  -- 2 levels
       ∃m₁∃m₂(...)) }  -- 3 levels, etc.

Output

For bounded depth: expressible. For unbounded depth: not expressible in pure TRC.

Explanation

TRC (and basic relational algebra) cannot express unbounded transitive closure. Each level requires explicit quantification. This limitation is why SQL added recursive CTEs.

advanced-patterns.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
-- ANTI-JOIN: Employees with no assignments
{ e | Employee(e) ∧ ¬∃a(Assignment(a) ∧ a.emp_id = e.emp_id) }
 
-- SEMI-JOIN: Departments that have at least one high earner
{ d | Department(d) ∧ ∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ e.salary > 100000) }
 
-- SECOND HIGHEST (without aggregates):
-- Find employees earning less than max, but more than all others below max
{ e | Employee(e) ∧ 
      ∃top(Employee(top) ∧ top.salary > e.salary ∧ 
           ¬∃above(Employee(above) ∧ above.salary > top.salary)) ∧
      ¬∃between(Employee(between) ∧ between.salary > e.salary ∧ 
                ∃top2(Employee(top2) ∧ top2.salary > between.salary ∧
                     ¬∃above2(Employee(above2) ∧ above2.salary > top2.salary))) }
 
-- Actually simpler: second highest = maximum of those below maximum
{ e | Employee(e) ∧ 
      ∃top(Employee(top) ∧ ¬∃t2(Employee(t2) ∧ t2.salary > top.salary) ∧ 
           top.salary > e.salary) ∧
      ¬∃e2(Employee(e2) ∧ e2.salary > e.salary ∧ 
           ∃top(Employee(top) ∧ ¬∃t2(Employee(t2) ∧ t2.salary > top.salary) ∧ 
                top.salary > e2.salary)) }

Pattern Library

Formula Transformation and Optimization

Complex formulas can often be rewritten into equivalent forms that are easier to understand, optimize, or execute.

De Morgan's Laws:

¬(P ∧ Q) ≡ ¬P ∨ ¬Q
¬(P ∨ Q) ≡ ¬P ∧ ¬Q

Quantifier Duality:

¬∃t(P(t)) ≡ ∀t(¬P(t))
¬∀t(P(t)) ≡ ∃t(¬P(t))

These allow converting between existential and universal forms.

Pushing Negation Inward:

¬∃e(Employee(e) ∧ e.salary > 100000)
≡ ∀e(¬(Employee(e) ∧ e.salary > 100000))
≡ ∀e(¬Employee(e) ∨ e.salary ≤ 100000)
≡ ∀e(Employee(e) → e.salary ≤ 100000)

"No employee earns more than 100K" becomes "All employees earn ≤100K."

Converting Universal to Negated Existential:

This is the most practical transformation for SQL:

∀t(R(t) → P(t))
≡ ¬∃t(R(t) ∧ ¬P(t))

"All R satisfy P" becomes "No R violates P." SQL implements this as NOT EXISTS.

Key Formula Equivalences
Original	Equivalent	Use Case
`∀t(R(t) → P(t))`	`¬∃t(R(t) ∧ ¬P(t))`	Universal to NOT EXISTS
`¬(P ∧ Q)`	`¬P ∨ ¬Q`	Negation distribution
`P → Q`	`¬P ∨ Q`	Implication elimination
`∃t(P(t)) ∧ ∃t(Q(t))`	`∃t(P(t)) ∧ ∃s(Q(s))`	Scope clarification
`∀t∀s(P(t,s))`	`∀s∀t(P(t,s))`	Quantifier reordering (same type)

formula-transformation.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- ORIGINAL: Departments where all employees earn > 50000
{ d | Department(d) ∧ ∀e(Employee(e) ∧ e.dept_id = d.dept_id → e.salary > 50000) }
 
-- STEP 1: Apply implication equivalence
-- ∀e(¬(Employee(e) ∧ e.dept_id = d.dept_id) ∨ e.salary > 50000)
 
-- STEP 2: Apply quantifier duality
{ d | Department(d) ∧ ¬∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ ¬(e.salary > 50000)) }
 
-- STEP 3: Simplify inner negation
{ d | Department(d) ∧ ¬∃e(Employee(e) ∧ e.dept_id = d.dept_id ∧ e.salary ≤ 50000) }
 
-- This form translates directly to SQL NOT EXISTS:
-- SELECT d.* FROM Department d
-- WHERE NOT EXISTS (
--     SELECT 1 FROM Employee e
--     WHERE e.dept_id = d.dept_id AND e.salary <= 50000
-- )

Optimization Insight

SQL Translation of Complex Formulas

Translating complex TRC formulas to SQL requires mapping each construct to its SQL equivalent. This section provides systematic translation patterns.

Existential Subqueries:

∃t(R(t) ∧ condition)  →  EXISTS (SELECT 1 FROM R t WHERE condition)

Universal Subqueries:

∀t(R(t) → condition)  →  NOT EXISTS (SELECT 1 FROM R t WHERE NOT condition)

Nested Quantifiers:

Each quantifier becomes a subquery, nested correspondingly.

complex-to-sql.sql

-- TRC: Find customers who have ordered ALL products
-- { c | Customer(c) ∧ ∀p(Product(p) → ∃o(Order(o) ∧ o.cust_id = c.id ∧ o.prod_id = p.id)) }
 
-- SQL Translation:
SELECT c.*
FROM Customer c
WHERE NOT EXISTS (  -- ∀p translates to NOT EXISTS (... NOT ...)
    SELECT 1 
    FROM Product p
    WHERE NOT EXISTS (  -- ¬∃o becomes NOT EXISTS
        SELECT 1 
        FROM Order o
        WHERE o.cust_id = c.id 
          AND o.prod_id = p.id
    )
);
 
-- TRC: Find employees earning more than everyone in Sales
-- { e | Employee(e) ∧ ∀s(Employee(s) ∧ s.dept_id = 'Sales' → e.salary > s.salary) }
 
-- SQL Translation:
SELECT e.*
FROM Employee e
WHERE NOT EXISTS (
    SELECT 1 
    FROM Employee s
    WHERE s.dept_id = 'Sales' 
      AND NOT (e.salary > s.salary)  -- e.salary <= s.salary
);
 
-- Alternative using ALL (SQL extension):
SELECT e.*
FROM Employee e
WHERE e.salary > ALL (
    SELECT s.salary FROM Employee s WHERE s.dept_id = 'Sales'
);

Correlated Subqueries:

This is precisely the bound-free variable relationship in TRC: inner quantified variables can reference outer free variables.

Multiple EXISTS:

Conjunctions of existentials become multiple EXISTS clauses:

TRC: ∃d(D(d) ∧ P(d)) ∧ ∃p(P(p) ∧ Q(p))
SQL: EXISTS (... D ...) AND EXISTS (... P ...)

Disjunction of EXISTS:

TRC: ∃d(D(d) ∧ P(d)) ∨ ∃p(P(p) ∧ Q(p))
SQL: EXISTS (...) OR EXISTS (...)

The NOT EXISTS Double Negation

Common Pitfalls and Debugging

Complex formulas are prone to subtle errors. Understanding common pitfalls prevents frustration.

Pitfall 1: Incorrect Quantifier Order

✗ "Some employee manages all projects"
  ∀p(Project(p) → ∃e(Employee(e) ∧ manages(e, p)))
  -- This says: Each project has SOME manager (possibly different)

✓ "Some employee manages all projects"
  ∃e(Employee(e) ∧ ∀p(Project(p) → manages(e, p)))
  -- This correctly says: ONE employee manages ALL projects

Pitfall 2: Missing Range Predicates

✗ { e | e.salary > 50000 ∧ ∃d(e.dept_id = d.dept_id ∧ d.budget > 1000000) }
  -- e has no range predicate! d has no range predicate!

✓ { e | Employee(e) ∧ e.salary > 50000 ∧ 
        ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.budget > 1000000) }

Pitfall 3: Variable Scope Confusion

✗ { e | Employee(e) ∧ (∃d(Department(d) ∧ e.dept_id = d.dept_id)) ∧ d.name = 'HR' }
  -- d is out of scope after the existential closes!

✓ { e | Employee(e) ∧ ∃d(Department(d) ∧ e.dept_id = d.dept_id ∧ d.name = 'HR') }
  -- All d references inside the existential scope

Debugging Checklist

•Range Check: Does every tuple variable have a positive range predicate (R(t))?
•Scope Check: Are all variable references within their quantifier's scope?
•Quantifier Order: Does the nesting match the intended reading (left-to-right)?
•Implication in Universals: Does ∀ use the pattern ∀t(R(t) → condition)?
•Target Variables: Are all variables in the target list free in the formula?
•Type Compatibility: Do all comparisons involve compatible types?
•NULL Handling: Could NULLs cause unexpected UNKNOWN results?

Debugging Strategy:

Start Simple: Write the simplest version of the query first
Test Components: Test subformulas independently
Add Complexity Gradually: Add one condition at a time, verifying each
Check Edge Cases: What if the quantified set is empty?
- ∃t(P(t)) over empty set → FALSE
- ∀t(P(t)) over empty set → TRUE (vacuously true)
Trace Evaluation: Manually evaluate with small sample data

Vacuous Truth

Real-World Complex Query Examples

Let's conclude with comprehensive real-world examples demonstrating the full power of complex TRC formulas.

Example 1: Supplier with Complete Red Parts Coverage

Business Need: Find suppliers who can supply all red parts in our catalog.

real-world-example-1.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
-- Schema:
-- Supplier(supplier_id, name, location)
-- Part(part_id, name, color)
-- Catalog(supplier_id, part_id, price)
 
-- TRC Query:
{ s | Supplier(s) ∧ 
      ∀p(Part(p) ∧ p.color = 'Red' → 
         ∃c(Catalog(c) ∧ c.supplier_id = s.supplier_id ∧ c.part_id = p.part_id)) }
 
-- English: A supplier s is in the result if and only if
--          for every red part p, there exists a catalog entry c
--          linking s to p.
 
-- SQL Translation:
SELECT s.*
FROM Supplier s
WHERE NOT EXISTS (
    SELECT 1 FROM Part p
    WHERE p.color = 'Red'
      AND NOT EXISTS (
          SELECT 1 FROM Catalog c
          WHERE c.supplier_id = s.supplier_id
            AND c.part_id = p.part_id
      )
);

Example 2: Employees Outearning Their Entire Management Chain

Business Need: Find employees who earn more than both their direct manager AND their manager's manager.

real-world-example-2.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
-- Schema:
-- Employee(emp_id, name, salary, manager_id)
 
-- TRC Query:
{ e | Employee(e) ∧ 
      ∃m(Employee(m) ∧ e.manager_id = m.emp_id ∧ e.salary > m.salary ∧
         ∃mm(Employee(mm) ∧ m.manager_id = mm.emp_id ∧ e.salary > mm.salary)) }
 
-- English: Employee e earns more than their manager m,
--          and m has a manager mm, and e earns more than mm too.
 
-- Note: This only considers 2 levels. For arbitrary depth, 
--       recursive constructs (not standard TRC) would be needed.
 
-- SQL Translation:
SELECT e.*
FROM Employee e
WHERE EXISTS (
    SELECT 1 FROM Employee m
    WHERE e.manager_id = m.emp_id
      AND e.salary > m.salary
      AND EXISTS (
          SELECT 1 FROM Employee mm
          WHERE m.manager_id = mm.emp_id
            AND e.salary > mm.salary
      )
);

Example 3: Departments with Balanced Teams

Business Need: Find departments where no employee earns more than double another employee's salary.

real-world-example-3.trc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- TRC Query:
{ d | Department(d) ∧ 
      ∀e₁∀e₂(Employee(e₁) ∧ Employee(e₂) ∧ 
              e₁.dept_id = d.dept_id ∧ e₂.dept_id = d.dept_id →
              e₁.salary ≤ 2 * e₂.salary) }
 
-- English: For all pairs of employees in department d,
--          neither earns more than double the other.
 
-- SQL Translation (using double NOT EXISTS):
SELECT d.*
FROM Department d
WHERE NOT EXISTS (
    SELECT 1 FROM Employee e1, Employee e2
    WHERE e1.dept_id = d.dept_id
      AND e2.dept_id = d.dept_id
      AND e1.salary > 2 * e2.salary  -- Violation of balance
);

Summary: Mastering Complex Formulas

Key Takeaways

•Connective Mastery: ∧ (and), ∨ (or), ¬ (not), → (implies) combine atoms into complex conditions with precise semantics
•Nested Quantification: ∃∃, ∃∀, ∀∃, ∀∀ patterns express multi-level relationships; quantifier order matters critically
•TRC-Algebra Equivalence: Each relational algebra operation has a TRC equivalent; they are expressively equal (Codd's theorem)
•Advanced Patterns: Division, maximum finding, counting, and set comparisons follow recognizable complex formula templates
•Formula Transformation: De Morgan's laws, quantifier duality, and implication elimination enable query optimization
•SQL Translation: EXISTS implements ∃; NOT EXISTS with inner NOT implements ∀; nested quantifiers become nested subqueries
•Debugging Discipline: Check range predicates, variable scope, quantifier order, and handle edge cases (empty sets, NULLs)

Module Complete!

This knowledge empowers you to:

Read and write formal database specifications
Understand SQL at its logical foundations
Reason about query equivalence and optimization
Recognize the declarative vs. procedural distinction
Prepare for advanced topics like Domain Relational Calculus and query optimization theory

Module Complete