[HD] EECS3342 F26 - 2026-10-01 (Thursday) - Lecture 7

Overview

Jackie Wang reviews relational algebra and function properties for EECS3342, showing how overriding replaces relation pairs and how to prove or disprove that a relation is functional. The lecture distinguishes partial from total functions by their domains, compares relational image with functional application, and explains the extra domain proof obligation generated by Rodin.

Key takeaways

Overriding R with T is equivalent to removing from R every pair whose first element lies in dom(T), then unioning the result with T.
A relation is functional exactly when it never contains two pairs with the same first element and different second elements; such a conflicting pair of pairs is a complete disproof witness.
A partial function from S to T requires functionality and dom(R) ⊆ S; totality strengthens this to dom(R) = S.
The nesting is total functions ⊆ partial functions ⊆ relations, because total functions satisfy both functionality and the relation definition.
Relational image returns a set, including the empty set when there are no matching pairs; applying a partial function returns a value only when the input is in its domain.
In Rodin, a function application g(C) carries the proof obligation C ∈ dom(g), while relational image does not require that domain condition.

Chapters

0:00 Programming Test, Lab Solutions, and Course Schedule

The single programming test is next Wednesday during each student's own enrollment session; Jackie Wang recommends attempting the Fall 2024 practice test under test-like conditions.
Lab 2 solutions include a PDF with mathematical specifications and a roughly 35–36-minute walkthrough; Lab 1 and Lab 2 solutions are relevant review material.
The class may finish injective, surjective, and bijective functions early next Tuesday before moving to the next topic.

3:00 Overriding Replaces Every Pair for Inputs in the Override Domain

For relations R and T, R overridden with T preserves R's pairs outside dom(T) and replaces all R-pairs whose first element is in dom(T).
With T = {(A,3), (C,4)}, dom(T) is {A,C}; relevant pairs in R for A and C are removed and replaced by exactly those two pairs.
A relation is a set of ordered pairs, so the order in which pairs are written has no semantic significance.

9:30 Using Overriding for Lab 1 Account Transfers

The balance variable B is a partial function from accounts to integers, and a transfer updates the balances for accounts ACC1 and ACC2.
Rodin events allow each variable to be assigned only once, so multiple balance updates should be expressed as one assignment using B overridden with a relation of changed account-balance pairs.
The overriding relation preserves every account balance not involved in the transfer.

13:00 Domain Subtraction Defines Overriding; Images Require a Range

The algebraic definition of overriding is (R domain-subtracted by dom(T)) union T: remove R's pairs on T's domain, then add T.
To compute the image of a set S under R, first restrict R to pairs whose first elements belong to S, then take the range: R[S] = ran(R restricted to S).
A domain restriction alone returns a relation, not the image set; image notation and range operations must have compatible types.

23:30 Functional Property: One Output at Most for Each Input

A relation is functional when any two pairs with the same first element also have the same second element.
For example, {(A,1),(A,3),(B,2)} is not a function because A maps to two distinct outputs; the empty relation is a function because it has no counterexample.
Functions form the subset of relations satisfying this property, while relations with a shared input and distinct outputs lie outside that subset.

30:00 Proving Functionality by Checking Every Pair

One proof strategy is to establish that R is empty, making the universal functional condition vacuously true.
For a nonempty relation, check its pairs and verify that no input is associated with more than one output.
The condition concerns outputs per input; it does not require every possible input to have an output.

34:00 Disproving Functionality with a Two-Pair Witness

A counterexample consists of (s,t1) and (s,t2) in R where t1 ≠ t2; this directly violates the functional property.
For {(A,1),(B,2),(A,3)}, the pairs (A,1) and (A,3) are a witness that the relation is not functional.
Removing either conflicting pair—for example, deleting (A,3)—eliminates that violation and can yield a function.

38:30 Partial and Total Function Notation in Rodin

The partial-function arrow denotes the set of all partial functions from source S to target T; the ordinary arrow denotes the set of all total functions from S to T.
A particular relation R is a partial function when it is functional and dom(R) ⊆ S.
A total function adds the stricter requirement dom(R) = S, so every source element has a defined output.

44:00 Partial Functions Allow Undefined Source Values

The condition dom(R) ⊆ S splits into dom(R) being a proper subset of S or exactly equal to S.
In the proper-subset case, some value in S is outside dom(R), so applying the function to that value is undefined.
The equal-domain case is precisely totality: every element of S has a range value.

49:40 Relations, Partial Functions, and Total Functions Form a Hierarchy

Relations are sets of ordered pairs with no functional constraint; partial functions are the relations that satisfy functionality.
Total functions are partial functions whose domain is exactly the source set S.
Thus every total function is also a partial function and a relation, but not every relation or partial function is total.

53:00 Rodin Type Checking: Set Membership Versus Subset

A single candidate relation R can be tested for membership in the set of partial functions from S to T.
A set containing candidate relations R1 and R2 is compared with that function set using subset, not membership.
In Rodin, using membership with a set of candidates on the left is a type error rather than a false proposition.

1:01:00 Classifying Relation Examples by Functionality and Domain

A relation such as {(2,A),(1,B)} is a partial function because neither input has multiple outputs.
A relation such as {(2,A),(3,A),(1,B)} is total from source {1,2,3}, since it is functional and its domain is the entire source.
A relation such as {(2,A),(1,B),(3,A),(1,A)} is not a partial function: input 1 has both A and B as outputs.

1:05:40 Why Total Functions Are a Proper Subset of Partial Functions

A partial function can have a domain smaller than S, whereas every total function covers all of S.
The set of all partial functions is therefore larger than the set of all total functions.
A function that is functional but omits a source value belongs to the partial-function set but not the total-function set.

1:07:30 Relational Image Versus Functional Application

For a partial function f = {(3,A),(1,B)} with source {1,2,3}, relational images are sets: f[{3}] = {A}, f[{1}] = {B}, and f[{2}] = ∅.
Functional application returns the individual outputs f(3)=A and f(1)=B, while f(2) is undefined because 2 is outside dom(f).
Relational image remains defined for an input with no matching pair by returning the empty set; function application may instead be undefined.

1:11:40 Rodin Generates a Domain Proof Obligation for Function Calls

A relation f applied using relational image to a constant C produces a set and is well-defined even when C is outside dom(f).
A partial function g applied as g(C) may be undefined, so Rodin generates the proof obligation C ∈ dom(g).
Choosing relational image or functional application depends on whether the expression should return a set of outputs or a single function value.

Summary, takeaways, and chapters were generated by AI from the video's transcript and may contain errors. The video belongs to its creator, Jackie Wang.