22:
176:"variable convention", requiring arbitrary renaming of variables during reduction to ensure that the "(x≠y and x not free in N)" condition on the last rule is always satisfied before applying the rule. Therefore many calculi of explicit substitution avoid variable names altogether by using a so-called "name-free"
216:
need to be very careful when dealing with substitutions. Without sophisticated mechanisms for structure-sharing, substitutions can cause a size explosion, and therefore, in practice, substitutions are delayed and explicitly recorded. This makes the correspondence between the theory and the
95:
in an implicit manner which is not expressed within the calculus; the "freshness" conditions in such implicit calculi are a notorious source of errors. The concept has appeared in a large number of published papers in quite different fields, such as in
220:
Once substitution has been made explicit, however, the basic properties of substitution change from being semantic to syntactic properties. One most important example is the "substitution lemma", which with the notation of λx becomes
318:
N. G. de Bruijn: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technological
University Eindhoven, Netherlands, Department of Mathematics, (1978), (TH-Report), Number 78-WSK-03.
217:
implementation highly non-trivial and correctness of implementations can be hard to establish. One solution is to make the substitutions part of the calculus, that is, to have a calculus of explicit substitutions.
267:
Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans; Birkedal, Lars (27 April 2017). "The
Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types".
40:
233:. Following this, a multitude of calculi were described trying to offer the best compromise between syntactic properties of explicit substitution calculi.
124:, namely the form M⟨x:=N⟩, which reads "M where x will be substituted by N". (The meaning of the new term is the same as the common idiom
204:, the idea of a specific calculus where substitutions are part of the object language, and not of the informal meta-theory, is traditionally credited to
188:
Explicit substitutions were sketched in the preface of Curry's book on
Combinatory logic and grew out of an ‘implementation trick’ used, for example, by
328:
M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit
Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375–416.
229:
A surprising counterexample, due to Melliès, shows that the way this rule is encoded in the original calculus of explicit substitutions is not
225:(M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (where x≠y and x not free in P)
58:
368:
Delia Kesner: A Theory of
Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)
394:
399:
389:
201:
84:
384:
346:
P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60–69.
337:
P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328–334
247:
230:
105:
276:
355:
K. H. Rose, Explicit
Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 (
242:
286:
212:, Curien, and Lévy. Their seminal paper on the λσ calculus explains that implementations of
97:
72:
213:
193:
177:
173:
121:
117:
101:
88:
76:
172:
While making substitution explicit, this formulation still retains the complexity of the
92:
378:
209:
290:
205:
356:
168:(λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y and x not free in N)
197:
133:
120:
with explicit substitution is "λx", which adds one new form of term to the
132:
M from many programming languages.) λx can be written with the following
189:
83:
if they pay special attention to the formalization of the process of
281:
15:
36:
31:
may be too technical for most readers to understand
192:, and became a respectable syntactic theory in
308:. Amsterdam: North-Holland Publishing Company.
8:
200:theory. Though it actually originated with
280:
59:Learn how and when to remove this message
43:, without removing the technical details.
259:
87:. This is in contrast to the standard
304:Curry, Haskell; Feys, Robert (1958).
91:where substitutions are performed by
41:make it understandable to non-experts
7:
269:Logical Methods in Computer Science
14:
146:x⟨y:=N⟩ → x (x≠y)
140:(λx.M) N → M⟨x:=N⟩
20:
1:
157:) ⟨x:=N⟩ → (M
416:
306:Combinatory Logic Volume I
143:x⟨x:=N⟩ → N
291:10.2168/LMCS-12(3:7)2016
161:⟨x:=N⟩) (M
116:A simple example of a
81:explicit substitutions
395:Operational semantics
248:Substitution instance
165:⟨x:=N⟩)
400:Substitution (logic)
231:strongly normalizing
106:symbolic computation
390:Rewriting systems
243:Combinatory logic
98:abstract machines
79:are said to have
69:
68:
61:
407:
369:
366:
360:
353:
347:
344:
338:
335:
329:
326:
320:
316:
310:
309:
301:
295:
294:
284:
264:
73:computer science
64:
57:
53:
50:
44:
24:
23:
16:
415:
414:
410:
409:
408:
406:
405:
404:
385:Lambda calculus
375:
374:
373:
372:
367:
363:
354:
350:
345:
341:
336:
332:
327:
323:
317:
313:
303:
302:
298:
266:
265:
261:
256:
239:
214:lambda calculus
194:lambda calculus
186:
178:De Bruijn index
174:lambda calculus
164:
160:
156:
152:
122:lambda calculus
118:lambda calculus
114:
102:predicate logic
93:beta reductions
89:lambda calculus
65:
54:
48:
45:
37:help improve it
34:
25:
21:
12:
11:
5:
413:
411:
403:
402:
397:
392:
387:
377:
376:
371:
370:
361:
348:
339:
330:
321:
311:
296:
258:
257:
255:
252:
251:
250:
245:
238:
235:
227:
226:
185:
182:
170:
169:
166:
162:
158:
154:
150:
147:
144:
141:
113:
110:
77:lambda calculi
67:
66:
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
412:
401:
398:
396:
393:
391:
388:
386:
383:
382:
380:
365:
362:
358:
352:
349:
343:
340:
334:
331:
325:
322:
315:
312:
307:
300:
297:
292:
288:
283:
278:
274:
270:
263:
260:
253:
249:
246:
244:
241:
240:
236:
234:
232:
224:
223:
222:
218:
215:
211:
207:
203:
199:
195:
191:
183:
181:
179:
175:
167:
148:
145:
142:
139:
138:
137:
135:
131:
127:
123:
119:
111:
109:
107:
103:
99:
94:
90:
86:
82:
78:
74:
63:
60:
52:
42:
38:
32:
29:This article
27:
18:
17:
364:
351:
342:
333:
324:
314:
305:
299:
272:
268:
262:
228:
219:
187:
171:
129:
125:
115:
85:substitution
80:
70:
55:
46:
30:
379:Categories
282:1606.09455
254:References
180:notation.
275:(3): 36.
202:de Bruijn
198:rewriting
134:rewriting
237:See also
210:Cardelli
190:AUTOMATH
112:Overview
49:May 2023
184:History
136:rules:
35:Please
104:, and
357:ps.gz
277:arXiv
206:Abadi
128:x:=N
196:and
287:doi
126:let
71:In
39:to
381::
359:).
285:.
273:12
271:.
208:,
149:(M
130:in
108:.
100:,
75:,
293:.
289::
279::
163:2
159:1
155:2
153:M
151:1
62:)
56:(
51:)
47:(
33:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.