Functional dependency

Satisfiesdef

A functional dependency X → Y holds when any two tuples agreeing on every attribute in X also agree on every attribute in Y. Normalisation theory is the study of which dependencies a schema forces.

def Satisfies {Attr Val : Type*} (r : RelationInstance Attr Val)
    (X Y : Set Attr) : Prop :=
  ∀ t ∈ r, ∀ u ∈ r, (∀ a ∈ X, t a = u a) → ∀ b ∈ Y, t b = u b

Builds on

Relation instance

import Conjectura.Defs.ComputerScience.Databases.FunctionalDependency · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits