MGU-SUBS - Most General Unifier and Substitution Project

This project provides an OCaml implementation for term manipulation including variable substitution, composition, and computing the Most General Unifier (MGU). The project is built around the main module in term_array.ml.

Project Overview

• term_array.ml: Implements the term data structure, unification, substitution (both regular and in-place), editing of terms, and related functionalities.
• Tests:
  • term_array_tests.ml: Basic test cases for term manipulation.
  • additional_tests.ml: Advanced and comprehensive tests covering edge cases.

Requirements

• OCaml compiler (e.g., ocamlc)
• GNU Make

How to Build and Run

1. Compile the Tests:

   • Run make to compile the project using the provided Makefile.

2. Run Basic Tests:

   • Execute the basic tests with:

     make run_tc
     

3. Run Advanced Tests:

   • Execute the advanced tests with:

     make run_advanced
     

4. Run All Tests:

   • To run all available tests:

     make run_all
     

5. Clean Compiled Files:

   • Remove generated files with:

     make clean
     

Detailed Implementation

The core functionality is implemented in term_array.ml. Key components include:

• Term Representation:
  Terms are defined as either a variable (V string) or a node (Node(symbol * term array)).
  • A symbol is a pair of its name and arity.
  • Terms are built using arrays to efficiently handle children.

• Signature Validation:
  A signature is an array of symbols. The function checks that each symbol has a non-negative arity and ensures no duplicate symbol names exist.

• Well-formed Term Checking:
  The function wfterm verifies that a term conforms to a given signature by checking that the symbol’s provided arity matches both the expected arity and the number of child terms.

• Unification (MGU):
  The mgu function computes the Most General Unifier of two terms. It recursively applies substitutions, ensuring no circular bindings occur by using an occurs-check. Two exceptions, NEGATIVE_ARITY and NOT_UNIFIABLE, signal errors related to signature and unification failures, respectively.

• Substitution Mechanisms:
  • Regular Substitution:
  Implemented via the subst function, this applies an association list mapping variables to terms.
  • Substitution Composition:
  The compose_subst function combines substitutions, ensuring that mappings are applied in the correct order.
  • In-place Substitution:
  Through a mutable reference (term_ref), the subst_in_place function updates a term directly, offering an alternative to traditional substitution.

• Editing Terms:
  The edit function replaces a subterm at a specified position (given as a list of indices) with a new term, enabling dynamic term modifications.

• Supporting Utility Functions:
  Additional functions compute the term's height (ht), size (size), and gather its variables (vars).
  String conversion functions help in visualizing both terms and substitutions.

Happy coding!