mudri

@JanusBahsJacquet I don't think Japanese is a good counterexample. For a lot of related native words, the kanji they're written with don't reflect their etymology. For example, 男 otoko splits up into oto + ko (子). The same oto is found in 乙女 otome and possibly 大人 otona, originally meaning “young”. As for the distinguishing part, me consistently means “female”, but ko doesn't really mean “male” on its own; it just means “little” or “child”. Similar female-marking happens in several Sinitic words, such as 少年 “boy” (literally small years) vs 少女 “girl” (literally small female).

However, I would expect that real SML implementations don't use term rewriting to run programs, and instead compile any terms to bit representations and machine code instructions. Thus, when you run the executable of your NbE algorithm created by your SML compiler, no substitution really happens. There's clearly no substitution directly on object language terms – because we never defined it – and there's no substitution on ML terms because it doesn't happen to be implemented that way. The only substitution is in the reference semantics of SML, which we don't run directly.

@GuyCoder I don't really understand what you're asking in your penultimate comment. NbE is a normalisation methodology, meaning that it maps convertible terms to equal terms (up to α-equivalence). This gives you “modulo convertibility” for free. The specific representation of binders is, to some extent, a separate concern, as long as deciding α-equivalence on it is easy enough. IIRC, de Bruijn levels are performant in practice.

@GuyCoder For your last comment, to be specific I'll talk about the NbE procedure listed on the Wikipedia page. The metalanguage is Standard ML, and the object language is STλC with functions and products. Notice that there is no definition of substitution (on the object language) listed. The place where we could imagine substitution happening is in the metalanguage, where reduction of Standard ML may be implemented by repeatedly applying operational rules to the program until no more apply. This is what we tend to do when reasoning about SML programs. (contd)

@GuyCoder My way of speaking was somewhat loose, though it leads to a good slogan. If the metalanguage is functional, we will usually think of its semantics as being given by a small step operational semantics, including β-rules defined via substitution. In practice, we'll probably compile metalanguage programs into machine code such that no substitution actually happens (e.g, using stack frames to pass arguments). See the meaning of app (s, t) in particular (in the linked Wikipedia page), where if S is a λ-expression, we will get a β-reduction.

I think the trick with NbE is to use the metalanguage's substitution rather than defining your own on the object language. I don't know whether this covers every use case of substitution in a proof assistant, but it seems like a promising route for an answer.