• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Recursion-and-induction

R-and-i-substitutions

Recursion and Induction: Substitutions

A substitution  is a set {v_0  ← t_0, v_1  ← t_1,  …} where each v_i  is a distinct variable symbol and each t_i  is a term. If, for a given substitution σ  and variable v, there is an i  such that v  is v_i, we say v  is bound  by σ. If v  is bound by σ, then the binding  of v  in σ  is t_i, for the i  such that v_i  is v. (In set theory, a substitution is just a finite function that maps the v_i  to their respective t_i.)

The result of applying  a substitution σ  to a term term  is denoted term/σ  and is defined as follows. If term is a variable, then term/σ  is either the binding of term  in σ  or is term  itself, depending on whether term  is bound in σ. If term  is a quoted constant, term/σ  is term. Otherwise, term  is (f  a_1   …  a_n) and term/σ  is (f  a_1/σ   …  a_n/σ).

Problem 6.
Suppose σ  is

{x ← (car a), 
 y ← (cdr x)}

What term is (car (cons x (cons y (cons '"Hello" z))))/σ?

Next: Abbreviations for Terms (or Table of Contents)