121 3NF

Informally, Third Normal Form, or 3NF, says that a non-key attribute should not depend on another non-key attribute.

Example which violates 3NF

The following relation has the key {emp_id}:

Assume the following functional dependencies hold:

• {emp_id} → {dept_id} because each employee is assigned to one department
• {dept_id} → {dept_name} because each department identifier has one department name

The repeated department names make the transitive dependency visible.

The same modelling mistake can be written in Predica. The RM-style attribute names become contextual inside the Employee type, so emp_id is written as id:

entity Employee
{
    Integer id;
    Integer dept_id;
    String dept_name;

    key {id};
}

Here dept_name does not depend directly on the key. It depends on another non-key attribute, dept_id, which is being used as an identifier for an unmodelled department.

Writing the dependency as a constraint

If the model is left in this shape, the dependency from department identifier to department name has to be imposed over the containing collection of employees. One way to write it is to say that there is no pair of employees with the same department identifier and different department names:

entity Company
{
    Employee employee*;

    constraints
    {
        let company = this in
            employee.(let e = this in
                company.employee.[
                    dept_id = e.dept_id
                    ∧ dept_name ≠ e.dept_name
                ].Σempty);
    }
}

This constraint is the Predica form of {dept_id} → {dept_name}. It is non-local because the department name is repeated on employee records instead of being a local fact about a department.

Fixing the violation

The fix is to separate the facts about employees from the facts about departments. In relational form, this decomposes the original relation into two relations:

In Predica, the same repair is to model Department explicitly:

entity Department
{
    Integer id;
    String name;

    key {id};
}

entity Employee
{
    Integer id;
    Department dept;

    key {id};
}

entity Company
{
    Department department*;
    Employee employee*;
}

After this repair, the cross-employee FD constraint is no longer needed. The department name is a local attribute of Department, and each employee points to the department they belong to.