Questions tagged [substitution]
Questions regarding syntactic substitutions should be tagged with this.
4
questions
4
votes
1
answer
100
views
How to encode and manipulate (parallel) substitutions?
While attempting to formalize some basic properties of STLC I fell into a very deep rabbit hole revolving around substitutions. Apparently there are a few different ways to go about it, including ...
- 299
5
votes
0
answers
205
views
An algorithm for the substitution of formulas for predicates in first order logic
I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
- 419
4
votes
0
answers
131
views
Are there any proof assistants that can not be derived from substitution?
Are there any type of proof systems that can not be implemented with substitution at the core?
In essence if I want to implement a base library for building up various proof assistants do I only need ...
- 2,826
17
votes
2
answers
373
views
How to deal with Binders?
When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
- 1,098