317:-style interpretation of propositions, says that the meaning of a proposition arises from its introduction and elimination rules. Focalization refines this viewpoint by distinguishing between positive propositions, whose meaning arises from their introduction rules, and negative propositions, whose meaning arises from their elimination rules. In focused calculi, it is possible to define positive connectives by giving only their introduction rules, with the shape of the elimination rules being forced by this choice. (Symmetrically, negative connectives can be defined in focused calculi by giving only the elimination rules, with the introduction rules forced by this choice.)
63:
22:
165:
328:
interpretation of propositions to give them constructive content. For example, a realizer for the proposition "A implies B" is a computable function that takes a realizer for A, and uses it to compute a realizer for B. Realizability models characterize realizers for propositions in terms of their
321:
342:, given a computational system with nontermination and error stops as effects, realizability and focalization give the same meaning to types.
364:
at the time of its writing. And, thus, it offers to readers the possibility to understand ludics independently of their backgrounds.
223:
205:
146:
49:
84:
360:(such as illustrations of skunks). It has to be noted that the intent of these features is to enforce the point of view of
387:
407:
127:
391:
99:
306:
The primary achievement of ludics is the discovery of a relationship between two natural, but distinct notions of
183:
106:
80:
73:
35:
283:
and proof behaviours by following the paradigm of interactive computation, similarly to what is done in
261:
113:
300:
175:
95:
357:
333:
280:
249:
324:
of propositions, takes the view that we fix a computational system up front, and then give a
361:
349:
296:
252:. Key features of ludics include notion of compound connectives, using a technique known as
292:
288:
284:
245:
401:
325:
120:
339:
336:
237:
307:
291:
and focusing on their concrete uses—that is distinct occurrences—it provides an
273:
187:
62:
41:
374:
346:
356:, has some features that may be seen as eccentric for a publication in
314:
329:
visible behavior, and not in terms of their internal structure.
158:
56:
15:
313:
The first view, which might be termed the proof-theoretic or
287:
to which it is closely related. By abstracting the notion of
320:
The second view, which might be termed the computational or
354:
Locus solum: from the rules of logic to the logic of rules
87:. Unsourced material may be challenged and removed.
378:: from the rules of logic to the logic of rules
279:More precisely, ludics tries to retrieve known
8:
186:. There might be a discussion about this on
382:Mathematical Structures in Computer Science
244:is an analysis of the principles governing
50:Learn how and when to remove these messages
322:Brouwer–Heyting–Kolmogorov interpretation
224:Learn how and when to remove this message
206:Learn how and when to remove this message
147:Learn how and when to remove this message
7:
260:(invented by the computer scientist
85:adding citations to reliable sources
14:
31:This article has multiple issues.
352:. His paper introducing ludics,
163:
61:
20:
72:needs additional citations for
39:or discuss these issues on the
1:
345:Ludics was proposed by the
424:
394:(a wiki about Locus Solum)
392:Carnegie-Mellon University
384:, 11, 301–506, 2001.
299:, as loci can be seen as
272:over a base instead of
332:Girard shows that for
388:Girard reading group
176:confusing or unclear
81:improve this article
281:logical connectives
184:clarify the article
408:Mathematical logic
358:mathematical logic
310:, or proposition.
264:), and its use of
262:Jean-Marc Andreoli
250:mathematical logic
234:
233:
226:
216:
215:
208:
157:
156:
149:
131:
54:
415:
362:Jean-Yves Girard
350:Jean-Yves Girard
297:computer science
229:
222:
211:
204:
200:
197:
191:
167:
166:
159:
152:
145:
141:
138:
132:
130:
89:
65:
57:
46:
24:
23:
16:
423:
422:
418:
417:
416:
414:
413:
412:
398:
397:
373:Girard, J.-Y.,
370:
293:abstract syntax
246:inference rules
230:
219:
218:
217:
212:
201:
195:
192:
181:
168:
164:
153:
142:
136:
133:
90:
88:
78:
66:
25:
21:
12:
11:
5:
421:
419:
411:
410:
400:
399:
396:
395:
385:
369:
368:External links
366:
285:game semantics
232:
231:
214:
213:
171:
169:
162:
155:
154:
69:
67:
60:
55:
29:
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
420:
409:
406:
405:
403:
393:
389:
386:
383:
379:
377:
372:
371:
367:
365:
363:
359:
355:
351:
348:
343:
341:
338:
335:
330:
327:
326:realizability
323:
318:
316:
311:
309:
304:
302:
298:
294:
290:
286:
282:
277:
275:
271:
267:
263:
259:
255:
251:
247:
243:
239:
228:
225:
210:
207:
199:
189:
188:the talk page
185:
179:
177:
172:This article
170:
161:
160:
151:
148:
140:
129:
126:
122:
119:
115:
112:
108:
105:
101:
98: –
97:
93:
92:Find sources:
86:
82:
76:
75:
70:This article
68:
64:
59:
58:
53:
51:
44:
43:
38:
37:
32:
27:
18:
17:
381:
375:
353:
344:
340:linear logic
334:second-order
331:
319:
312:
305:
278:
274:propositions
269:
265:
258:focalisation
257:
253:
241:
238:proof theory
235:
220:
202:
193:
182:Please help
173:
143:
134:
124:
117:
110:
103:
91:
79:Please help
74:verification
71:
47:
40:
34:
33:Please help
30:
376:Locus solum
303:on memory.
178:to readers
107:newspapers
36:improve it
266:locations
42:talk page
402:Category
380:(.pdf),
347:logician
301:pointers
289:formulae
254:focusing
196:May 2012
137:May 2012
96:"Ludics"
315:Gentzen
174:may be
121:scholar
337:affine
242:ludics
123:
116:
109:
102:
94:
128:JSTOR
114:books
308:type
295:for
270:loci
100:news
390:at
268:or
256:or
248:of
236:In
83:by
404::
276:.
240:,
45:.
227:)
221:(
209:)
203:(
198:)
194:(
190:.
180:.
150:)
144:(
139:)
135:(
125:·
118:·
111:·
104:·
77:.
52:)
48:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
