### Abstract

This theory provides a formalization of substitutions on \(\lambda\)-free higher-order terms, establishing a structured framework with the expected algebraic properties. It introduces a type construction for the rigorous definition and manipulation of substitutions. The main theorem of this theory proves the existence of fixed-point substitutions under acyclicity, a theorem that is too often regarded as trivial in the literature.

### License

BSD License

### Topics

- Logic/Rewriting

### Session Substitutions_Lambda_Free

- Substitutions_Lambda_Free

### Depends on

- Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
- Well-Quasi-Orders

### Auto-related entries

- An Algebra for Higher-Order Terms

## Cite

×

Substitutions_Lambda_Free-AFP

    @article{Substitutions_Lambda_Free-AFP,
      author  = {Vincent Trélat},
      title   = {Substitutions for Lambda-Free Higher-Order Terms},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Substitutions_Lambda_Free.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest