La formation des notions en logique combinatoire

A C T A U N I V E R S I T A T I S L O D Z I E N S I S _____ FOLIA PHILOSOPHICA 7. 1990,

Je a n - P ie r r e G in i s t i

LA FORMATION DES NOTIONS EN LOGIQUE COMBINATOIRE

O'une m aniére g é n é ra le , par "fo rm a tio n ďes n o t io n s " , on peut entendre le u r c o n s tr u c tio n h is t o r iq u e , la m aniére dont pour la p rem iere f o is e l l e s ont é té p ro d u ite s , mais a u s s i to u te in ­ v e s t ig a t io n qui le s r e tro u v e . I I У a a lo r s a u ta n t de fo rm a tio n s qu'on e s t cap ab le h e u ris tiq u e m e n t d 'e n íma- g in e r e t q u 'i l у a d 'o b j e c t i f s d if f e r e n t e a a t t e in d r e . Ľ i d é e mSme q u 'i l у a u r a it des "b a s e s " d'un e approche m athématique e s t in e x a c te e t s t ^ r i l i s a n t e s i on le s c o n ę o it comme des p o in ts de d e p a rts in t a n g ib le s . C hercher des v o ie s n o u v e lle s v e rs des n o tio n s connues e s t un asp ect im portant du t r a v a i l ma- the'matique. On se propose de le m ontrer en exam inant l a manifere dont la lo g iq u e co m b in a to ire p a r v ie n t á r e t r o u v e r , dans un typ e de langage qui semble d 'a b o rd t r é s d i f f é r e n t , 1‘ im p lic a t io n ín t u i- t io n m s t e e t sea p r o p r iá t á s '.

Nous commencerons par p re s e n te r p lu s ie u r s n o tio n s de la thdorie des co m b in a te u rs, sous la forme d 'u n langage fo rm e l, que nous a p p e lle ro n s L , dont ľ alp h ab e t comporte le s données s u iv a n te s :

- un ensemble E in f i n i dénombrabie ď é lé m e n ts : a, b, c , d, e , f , g, h, a ' , . . . , h ', a " , . . . ( d i t s " v a r i a b l e s " ) , I , K, W, С, В ( d i t s "com b inateurs e ílé m e n ta ire s "):

- une o p e ra tio n b in a ir e : * ( d i t e " a p p l i c a t i o n " ) ; - une r e la t io n b in a ir e : ----» ( d i t e " r é d u c t i b i l i t é " ) ; - deux symboles de p o n c tu a tio n : ( , ) ( d it e s " p a r e n t h e s e s ").

* H askel B. C urry e s t le p r in c ip a l promoteur de la lo g iq u e com­ b in a t o ir e , dés le s annáes 30. I I e s t 1' a u te u r, avec R o b ert Feye pour le prem ier volume, avec J . R M indley e t J . P S e ld in pour le s e ­ cond, de ľ ouvrage c la s s iq u e dans ce domaine: Com binatory L o g ic , Amsterdam, N orth -H olland P u b l. С о тр ., I , lfere ed. 1958, 2ёте ed. I960 ( auquel se fo n t nos r é f é r e n c e s ); I I , 1972.

Ne sont bien formées que le s e x p ressio n s déterniinées par le s r é g le s :

R F j : tou t élément de C e s t un term e;

RF^: s i x et y sont des term es, (x * y ) e s t un term e; R F j: s i x e t y sont des term es, x — ► y e s t une form u le.

* , y, z, w, ou ces mémes l e t t r e s avec apostrophes ou in d ic e s num ériques, sont dea m e ta v a ria b le s e t de'signent des termes quel- conques; (x * y ) , dans son sens le p lu s la r g e , in d iq u e que l'a d - jo n c tio n de y á x p ro d u it quelque e f f e t . Au lie u du mot "te rm e ", n eu tre e t g é n é ra l* on peut d ir e , en le s p é c if ia n t , "com binaison a p p lic a t iv e " (en b r e f , "co m b in a iso n ") . Pa r RFj une com binaison peut n 'a v o ir qu'un seu l élém ent; К , p. e x ., e s t une com binaison.

Par économie d 'e c r i t u r e , nous supprim erons désorm aís tou t usage de et tou te p a ir e de p aren th eses groupant le s termes deux par deux ve rs la gauche; (a • b) s ’ é c r ir a done ab, ( ( a * b) * c) s 'é c r i c a abc, (a * (b * c ) ) s ' é c n r a (b e ). Nous conviendrons a u ssi ď é c r ir e x — * у — »z . . . pour x-—* у , у — * г . . . Les ex p res­ sio n s de forme xy sont d it e s "m o lé c u le s " K I p. e x ., e s t une mole­ c u le ; K et I sont r e s p e c t ivement ľ argument de gauche e t ľ argument de d r o it e de 1 'a p p lic a t io n de K ä I . Une com binaison sans parenthé- se e st d it o " s u i t e " ; a, abc, p. e x ., sont des s u it e s .

A chacun des 3 com binateurs é lé m e n ta ire s e s t a s so c ié e une re g le ( o it e "de r é c r i t u r e " ) qui exprime la tra n sfo rm a tio n q u 'i l f a i t s u b ir á une c e r t a in e s u it e , exprimée en m é ta v a ria b le s . On a p p e lle “ r é c r it u r e " la com binaison obtenue par 1' a c tio n d'un com binateur sur la s u it e q u 'i l précéde:

nom de la re g le

fo rm u la tio n

de la re g le nom du com binateur p rese n t ( I ) I x —► X id e n t if ic a t e u r (é lé m e n ta ir e ) ( К ) K x y x é lim in a te u r (e 'lé m e n ta ire ) (W) Wxy — *• xyy d u p lic a te u r (é lé m e n ta ir e )

(С ) Cxyz — ► xzy perm utateur (é lé m e n ta ir e )

(В ) Bxyz — •» x (y z ) com positeur (é lé m e n ta ir e ) x, y , z é ta n t des termes quelconques, on a p. ex. (en numérotanlj le s arguments e t en in d iq u a n t le s r é g le s .employees) W ab -r^ ab b ; K IU — v I ; x — y in d iq u e ra que y s 'o b t ie n t de * ä ľ is s u e ďe

p lu s ie u r s r e c r it u r e s s u c c e s s iv e s . A in s i BIab-*-*-ab, car B lab — 7-* I (a b )

' 123 ( B ) ^

— »ab.

P lu s g é n é ralem e n t, on a p p e lle ra "com binateur (proprem ent d i t ) " to u t terme auquel e st a s so c ió e une r é g le de r é c r it u r e t e l l e que, s i X e s t ce terme, X *t . . . xn — ► y t . . . ym, ou y^ . . . yffl sont des com binaisons de X j, . . . , xn . A in s i, B I e s t un com binateur. Les v a lu u rs de n e t da ra sont d it e s resp e ctive m e n t " o r d r e " et "d e g ré " de X. I e com binateur sera d it " r e g u li e r " s i e t seulem ent s i у^ e s t Xj e t s i y,, . . . ym sont des com binaisons de x^, . . . , (X la is s e in v a r ia n t le prem ier argum ent). X, Y, v o ire avec indices, se ro n t des m é ta v a ria b le s de co m b in ateu rs. Un com binateur d 'o r d re n a p p liq u e á une s u it e ayant moins de n élém ents ne donne pas lie u ä r é c r it u r e , ap p liq u é ä une s u it e ayant p lu s de n elem ents i l la r é c r i t selo n la prem iére des deu* r é g le s de monotonie (gauche et d r o it e ) qu'on a d jo in t aux p r é c é d e n t e s s i x commence par un com­ b in a te u r e t s i x— »y , a lo r s :

(MG) quelque s o it z, x z —>yz. A in s i par (K ) e t (MG) Kabc —-*ac; (MD) quelque s o it z, z x — >zy. A in s i par (K ) e t (MD) a (K b c )—* ab. Le com binateur a g it á ľ in t e r ie u r ď u n e e x p ressio n donnée, mais aKbc ne se r é c r i t pas. On peut m o d ifie r L eri a jo u ta n t ou en s u b b U tu a rit c e r t a in s com binateurs á I , K, W, C, B, p. ex. S t e l que Sxyz — x z ( y z ) . Une q u estio n e s s e n t ie l le p o rte dans tous le s cas sur la complétude J e 1' ensemble.

Un ensemble | X | , . . . , XmJ de com binateurs e s t d i t “ com p let" (ou " e t r e une b a s e ") s i pour tou t ensemble f i n i | x j , . . . , xn J de v a r i a ­ b le s e t to u te com binaison 0 de ces v a r ia b le s , 11 e x is t e une com- b in a is o n Ц' de X j ...Xm, t e l l e que Q*xl . . . xR ---- Q.

On s a i t é t a b l i r ď une p a rt que { I , K, W, С, в } e s t une base, d 'a u t r e p a rt ( e t notaminent) que { « , W, С, В } en e st une a u s s i c a r 1 peut é tr e d e f i n i , e t done rem placé, par WK. On d i t en e f f e t qu« X Y s i e t seuleinent s i le d é f in is s a n t Y e s t une com binaison de X p Хда e t qui possede le meme r e g le de r é ­ c r i t u r e que X, le d e f i n i . A in s i, l x — - x ; WKx—* K x x — -x.

{ к , s } forme éyalem ent une base, tous le s com binateurs d if f é -re n ts de К dans | l , К , И, С, ß j é ta n t d á f in is s a b le s par K, S. Oe l a тёте m aniere, e s t une base to u t ensemble de com binateurs í X , ,

1 / i l

•••» V t e l 4ue K e t S s o ie n t d e f in is s a b le s p ar X j , . . . , Xm (ou id e n tiq u e s d l 'u n des X^, . . . , X ^ ). On démontre qu'aucune base ne comporte moins de deux elem en ts.

Notons, pour e x p lo it a t io n u lt é r ie u r e , que dans chacun de ces lungages, chaque exp ressio n e s t obtenue á p a r t ir de X , ... X

1 1 m

par a p p lic a t io n , e t q u 'on peut en dormer une c o n s tru c tio n ( d i t e “ norm ale” ) en prenant le s termes dans l 'o r d r e , qui e st unique, determ ine par le s c o n d itio n s su ivan

tes-(1) le s arguments d'une a p p lic a t io n avant ľ a p p lic a t io n e lle - -méme;

(2) le s arguments ä gauche d'un argument donné avant c e t a rg u ­ ment;

(3 ) cnaque n o u v e lle o ccurrence d'un terme e s t t c s it e e comme s ' i l s 'a g i s s a i t d'un terme nouveau.

C e tte c o n s tru c tio n peut s 'e x p rim e r sous la forme d 'un arb re d é d u c t if. On e c r ir a Y la form ation de XY, d it e " l a c o n c lu s io n ", á p a r t i r de X, d it e “ la m ajeure” , e t de Y, d it e " l a m in eu re". A i n s i , par rap p o rt ä la base { K , s } l'e x p r e s s io n K (S K ) se c o n s tr u ir a :

J L _ S _________ 3, К

1. К 4. SK

5. K (S K )

Nous proposerons i c i p lu s ie u r s moyans sim ples p erm ettant de farm er ces bases de com binateurs. I I e s t v r a i qu'on pourra e stim e r ces r é s u lt a t s a la f o is tro p n a t a r e ls e t pas assez, D'une p a r t , en e ť f e t , le s procédés ob tie n n e n t des bases assez t r iv ia le m e n t , d'autre p a rt de norubreux com binateurs formes p ourront é tr e q u a l if ie s d 'a r- t i f i c i e l s , au sens ou C urry juge t e l le com binateur J ayant la re g le de r é c r it u r e Jx y z w — »x y (x w z ). T o u te fo ia , comme on le v e r r a , l l s perm ettent de p ro d u ire , sous des c o n d itio n s donne'es, des systém es axiom atiques complete pour c e r t a in e s lo g iq u e s formu- lé e s en dehors d'une approche c o m b in a to ire , dunt l'o b t e n t io n peut Ŕ tre raoins t r i v i a l e que c e l l e des com binateurs qui s e rv e n t ä 1' ob- t e m r .

Wous p rásen tero n s s u rto u t des rem plaęants de K. l l s dompor- ie ro n t des com binateurs ä e f f e t d 'é lim in a t io n , un com binateur étant le i s i e t seulement s i dans l'e x p r e s s io n de sa re g le de re'cri- tu re une des v a r ia b le s au moins de la s u it e ne fig u r e pas dans 1з ( r e c r i t u r e . En e f f e t , aucune com binaison de com binateurs p r i m i t i f s dont aucun n ’ a d 'e f f e t d 'é lim in a t io n ne p e rm e ttra it de d é f i n i r K a u is q u 'á aucurie étape des r é c r it u r e a e ffe c tu é e s par ces combinateurs

l e nonbre des o ccu rre n ce s d'une v a r ia b le ne d é c r o ít . Nous cher- cheruns au ssi ä f a i r e d r o it á la form ation h e u r is t iq u e des n o tio n s en cause, pour i l l u s t r e r une d is t i n c t io n f a i t e précédemment. N otre p re s e n ta tio n sera done v o lo n ta ire m e n t moins épure'e q u 'e l l e d e v r a it

1' e tr e á d 'a u t r e s ég ard s, e t a f in de r e s t it u e r justem ent la m anie­ re dont V e s p r it chemine. On peut p roced er p. ex. en g e n e 'ra lis a n t le cas s u iv a n t: s i A et A' ont des r e g ie s de r e 'c r it u r e t e l i e s que A 'a b — »abb, Aabb— » a , c.-a-d. sont i d e n t i f i e s par A 'x y — * x y y , A y y z — * x, i'e x p r e s s io n A'A d é f in ir a К puisque A 'A x y — * Axxy---* x . Ge lá {a * (c . - a - d .

W),

A, S } e s t une base. £n o u tre , comme on sa it d^f im r S par

W,

С, В ou par

w,

B ' (c .- á - d . C B ), sont a u s s i dee bases { a , U, С, в } e t | a , m, b '] .

La méthode c ó n s is te évidemment a rem p lacer К par une s o rte d e x ten sio n de К, c .- a - d . par un com binateur X qui o b tie n t une r é c r it u r e ne co n serva n t que le p rem ier argument, comme le f a i t K, raais d o rd re s u p é rie u r a c e lu i de K, aprés s 'e t r e donné un combi­ n ate u r X' qui commence par o b te n ir de la s u it e xy imposée pour X 'X , grace á un c e r t a in nombre de r é p e 't it io n s , une com binaison de degré egal ä ľ o rd re de X. P lu s g énéralem ent, s i X » s t t e l que Xxj . . . * n— ~» X j, on a K * df X 'X s i : ( a ) X' e t X sont des com- b in a tu u rs r é g u lie r s , (b ) ľ o r d r e de X 'e s t 2 ou 3, ( c ) le degré de X ’ e s t au moins 3 e t le deuxiéme élém ent de la r e 'c r it u r e e s t y, (d ) la r é c r it u r e obtenue par X ' sur Xxy comporte au moins 3 termes a u tre s que X, ( e ) 1 'o rd re de X e s t ég al au nombre de termes autres que X que comporte la r é c r i t u r e obtenue par X ' sur Xxy, ( f ) la ré- c r i tú re de X e s t x .

En e f f e t , par ( a ) , ( b ) , ( c ) on a:

(<*) x'xy< »xyx'j . . . xjj, ou x'j . . . x^ sont des com binaisons de y, ou

([3) X xyz-- *xyx'j . . . x^, ou x'j . . . x^ sont des com binaisons de y, z, e t done pour ( « ) X' Xxy — Xxx' . . . x ^ y, oil x| * ' sont des com binaisons de x, pour ( P ) X 'X x y ---»Xxx', . . . x' , ou x ', . . . x'

I in 1 ш

sont des com binaisons de x, y. O r, par (d ) xx'. . . . x 'y e t xx‘

t I Ш 1

. . . com portent au moins 3 term es, done par ( e ) e t < f) Xxx'^ *** хтУ x * X* x\ ••• A in s i, e t e n tre a u tr e s , A' et A t e ls que A' xyz —~ * x y (y z )z y e t Axyzw —* x form ent avec S une base: A'Axy — ► A x (x y)yx x.

le s elem ents ď u n e s u it e sauf le p rem ie r, é lim in e tous le s éie'ments d'une s u it e sauf le d e r n ie r : Xxj . . . xn — *,xp . Sx on se donne par exemplc Axy— >y et le com binateur C, on а К = df CA c a r САху—> Аух —* x. I I s 'e n s u it que { c , A (c -a-d K í ) , s } e st une base, done a u s s i { C, A, W, B } , { c , A, W, B*}.

On peut g é n é r a lis e r ce r á s u lt a t . Pour tou t X t e l que Xxj . . . * n— » xn , i l e x is te un com binateur X ' t e l que X'Xxy-—^-*x. I I suf- f i t en e f f e t que X' a i t une ré g le de r é c r it u r e de la forme: X'xjx^xj —* xl * j ••• X j, oíi Xj . . . X j comporte n - I o ccu rre n ce s d» x^ (C 'e s t le cas p a r t i c u l í e r de X' pour le q u e l Xj . . . X j comporte un s e u l é lé m e n t).

pour A x yz — » z , on a A 'x y z — * xzz y, i l v ie n t A 'A x y -- » A y y x — > x, pour Axy zw -— > w, on a A 'x y z — » x z z z y, i l v ie n t A'Axy --- * Ayyyx —> x , e t c .

On p o u rr a it démontrer ce r é s u l t a t par re c u rre n c e . Une a u tre s o lu tio n sera en o u tre p résen tée p lu s lo in . Oans chacun de ces cas { A‘ , A, S } e s t une base.

S i on co n sid é re m aintenant un com binateur X t e l uue Xx, . . . x

i n

. . . xn — » xn_ j (oíi n > 2 ), on a K * dj X . . . X, oil X . . . X com- p o rte n - I o ccu rre n ce s de X. S o it Axyz— * y, on a AAxy— > x; a o it Axyzw— * z , on a AAAxy——►x, e t c . (c e qu’ une re c u rre n c e ob- t ie n d r a i t a nouveau). Notons qu'une s e u le r é c r it u r e in t e r v ie n t pour chaque e x p re ssio n . Oans chacuri de ces ca s , { a , S J forme une base. On va g é n é r a lis e r sur ее X e t donner une d e f in it io n de K ä p a r­ t i r d 'un com binateur X t e l que Xx^ . . . xn ~ » x . (ou 4 < n - 2 ).

C e tte s it u a t io n nous in té r e s s e ip arce q u 'e l le donne ľ o ccasio n d 'e x p l i c i t e r la m aniere dont h e u ristiq u e m e n t peut se former une base de n o tio n s . Ľ a tt e n t io n se tro u ve f o c a lis é e sur un c e r t a in c a s , i c i une v a le u r p a r t i c u l i é r e de i , la v a le u r n - l , qui o f f r e une s o lu tio n f a c i l e ou p lu s é lé g a n te (un s e u l com binateur y s u f f i t a rem placer K ), p u is la s o lu tio n s 'é te n d de p a rt e t d 'a u t r e , ccrnne un c ris ta l- g e rm e le f a i t dans une eau^mére, i c i d 'un c ô té ä i * n, de ľ a u t r e c o té b i < n - 2, parce qu'on s 1e s t aperęu que la form ule donnant la s o lu tio n du cas in it ia le m e n t co n s id é re peut re- c e v o ir des a jo u ts qui la rendent p ropre ä t r a i t e r des a u tre c a s , e t merne s i c 'e s t au p r ix de sa prem iére s im p lic it é . Oés l o r s , sa tro u ve n t rele g u és c e r t a in s r é s u lt a t s obtenus pour d 'a u t r e s cas* (comme i c i d’ une p a rt pour i = l , d 'a u t r e p a rt pour i я n ) qui n 'o n t pas s u s c it é , méme s ' i l s l 'a u r a i e n t p u , le s mémes

develop-penients, mais auxquels i l peut a r r i v e r de p ré p a re r ia vo ie au tra ite m e n t d { í f i n i t i f en o f f r a n t , comme i c i , des s o lu tio n s v o is i- nea. Sans doute f a u t - i l rep rend re aprés coup le s r é s u lt a t s pour le u r donner ďem b'lée une fo rm u la tio n p lu s s a t is f a is a n t e mais i l demeure in te 're s sa n t a u s s i ď e x p l i c i t e r le s processu s psychologique- ment fo rm a teu rs, s i m a la d ro its s o i e n t - i ls .

S o it un com binateur X t e l que Xxj . . . xn — » ( l £ i < n ) e t s o it le s com binateurs

C XjX2X j — »■ X j X j*2

e t ^ l xl x2x3x4 * x2x3 * 4 * l1

t'2 x l x2x3x4 — * х2хз ж4х| х i> e t c . , en g é n é ra l

l x2x3x4 — * x2* 3X4X i ” • X1 xl * * ’ X1 comporte h o c­ cu rre n ce s de X j ) , e t en supposarit to u jo u rs e x clu s n - 1 c a r aucun com binateur ď o r d r e l n 'a ď e f f e t ď e lim in a t io n , e t le combina­ teu r X t e l que X x y — * x qui se confond avec K. I I v je n t a lo r s :

П ) s i i - n - 1, K = ^ X . . . X, ou X . . . X comporte n - 1 oc­ c u rre n ce s de X; (2 ) s i i = n, K * C(X . . . X ), ou X . . . X comporte n - I o c ­ c u rre n c e s de X; (3 ) s i i c n - 2, K ^ df C^X(X . . . X ) , ou X . . . X comporte i oc­ c u rre n ce s de X a t oii h = (n - I ) - i .

En e f f e t , Q ) peut s 'o b t e iu r , comme on ľ a vu, par re c u rre n c e , ega leme n t en ra iso n n a n t sur le s cas

suivants.-pour A x iX j *—* x2 CAxy —♦ Ayx ■— » x K

* df CA pour A x ^ X j -- « x y C (A A )x y — - AAyx —r» x K

1 df C(AA) pour A x 1x2 Ä 3x4 -- * x4 C(AAA)xy — »AAAyx — ► x K _{r df} C(AAA) A fin ď é t a b l í r (3 .), co n sid é ro n s une e x p re s s io n de forme (ос): X . . . Xxy e t le s e x p re s s io n s (0 ) C jX (X . . . X ), ou X . . . X comporte une o ccu rren ce de X en moins que dans ( d )

(p 1) C2X(X . . i X ) , ou X . . . X comporte deux o c c u rre n ce s de X en moins que dans (ex). Oans (ot) le X de t é t e posséde le s n arguments que l u i a t t r ib u e sa r e g le de r é c r it u r e , e t x e s t a la p la c e n - l , d 'a p ré s O ) . Or:

C jX (X . . . X)xy se r é c r i t ( у ) : X . . . XxyX, C2X(X . . . X)xy se r é c r i t ( у 1): X . . . XxyXX e t r .

merne nombre ď arguments que dan« ( a ) puisque C jX , C2X, e t c . p la ­ cent ä d r o it e de 1 'exp ressio n X . . . Xxy exactement le nombre de X q u 'e l l e comporte en moins sur sa gauche que dans ( a ) . D 'a u tr e part, x e st dans ( y ) , avec C jX , á la p la ce (n - 1) - l , c .- a - d . n - 2, dans (jrO, ov-ec C2X, á la p la ce (,n - I ) - 2, c.- a - d . n - 3, e t c . , p u is q u 'il у a resp ectivem en t 2 arguments é la d r o it e de x, 3 arguf- ments á la d r o it e de x, e t c . , done avec C^X ä la p la c e (n I ) -* i , i é ta n t selo n (3 ) chacune des v a le u rs é g a le s ou in f é r ie u r e s a n - 2. E n fin , dans ( y ) , ( j ' ) , e t c . le X de te te r é c r i t x la s u it e q u 'i l precéde s i X e s t t e l que, re a p e c tiv e m e n t: Xx^ . . . x(i

—* xn_2: Xxi xrT— * xn-3* e t c ’ 0° nc s l i c n - 2, ľ exp ressio n С^Х(Х . . . X)xy o b tie n d ra x á la p la c e donnée pour i par X. Un aura C^X ( X . . , X)xy — -*-*x. S o it p. e x .:

Axlx2x3~—*■ x2

AAxy —*• x

cf. ( 1)

К = df АА

AXjX^x^ ■

* x^

Cj AAxy —*• AxyA —» x

cf. (3)

к = df ĽjAA

^X1X2X3X4—* x3—* AAAxy —»x

cf. (I)

к

^*1х2хз*д ,-x2

CjA(AA)xy —► AAxyA —»x

cf. (3)

к = df CjA(AA)

AXjX2XjX^Xę—»Xj C j AAxy —► AxyA А А —* x

cf. (3)

к = df CjAA

Nous nous somuies in te 're s sé s aux rem plagants de X ( e t seulem ent d’ une c e r t a in e c la s s e ) . I I e s t p o s s ib le au ssi de tro u v e r des rem- p la ę a n ts de S. A in s i pour A x ^ X j X ^ — » x l x2x3x4^x3x4^ e t x 1X2X3X4 — -x^XjX^, S = df AA' puisque AA'xyz-— * A 'x y z ( y z ) — * x z (y z ).

Dana la th é o r ie des com binateurs qu'on v ie n t d ' e x p lo re r, le s e n t it é s sont a u ssi peu d iffe 'r e n c ié e s que p o s s ib le . Dans la seconde p a r t ie du programme c o m b in a to ire , au c o n t r a ir e , la th é o r ie d it e "de la f o n c t io n n a lit é ” , e l l e s vont é tr e c la s s é e s en c a t e g o r ie s .

On se donne des c a tá g o rie s p r im it iv e s , в ^ , 8^, . . . convenant aux o b je ts d'un c e r t a in domaine, expritné en un langage a p p lic a t if . On le s a t t r ib u e ä c e r t a in s o b je ts de ce domaine, en é c r iv a n t p. ex.

V,

62^x y^> Q,J’ on peut l i r e "x e s t un 8^*, "xy e s t un S 2" . Sur ces données, on o b tie n t d 'a u t r e s ca te 'g o rie s du domaine e t le u r a t t r i b u ­ tio n ä c e r t a in s o b je ts , gráce ä un o p é ra te u r F (q u i n 'e s t pas un co m b in ateu r) t e l que:

( l ) s i « et ß sont des c a t e g o r ie s , a lo r s Focß e s t une c a tł^ g o rie ; (.2) s i a (x y ) e t (3y , a lo r s Fpax, p.-&-d. s i xy e s t un o< e t y uęi p, x e s t un F<3a: ou (2 * ) qui permute dans (2 ) la majeure e t la c o n clu sio n (a v e c r e s t i t u t i o n de ľ o rd re a , ß , des v a r i a b l e s ) :

C 2 ') s i Fotßx e t o f y , a lo r s /Э(ху): Nous a p p e lle ro n s ( 2 ' ) “la r e g le ( F ) “. E l l e o b tie n t la c a te g o rie d’ un terme compose "a p a r t i r de c e lle s de ses cumposants; a e t p sont des m étavariab les de c a t e g o r ie s . En se ro n t a u s s i y, ď , 01' ...ď, a . . . Pour c e r t a in s tra ite m e n ts , comme ceux qui s u iv e n t, on peut s 'o x p n m e r a 1’ a id e des s e u le s m é ta v a ria b le s (c .- a - d . en termes géneraux) en la is s a n t S j , в 2 , . . . sans em p loi. Faßx se comprendra comme s ig n i- f i a n t "x a p p a rtie n t á la c a te'g o rie Faß des o b je ts dont chacun, ap p liq u e á un o b je t de la c a t e g o r i e a , determ ine un o b je t de la c a te 'g o iie |3" ; Fa ß s e ra d it "exp rim er un c a r a c t e r e fo n c tio n n e l de x ", c .- a - d . son type de fo n c tio n , e t par rap p o rt a des p rem isses donnéea. Oans une e x p ressio n de forme Fotßx, x e s t d it " l e s u j e t " , F « p " l e p r é d ic a t " .

Par ( 2 ) , on peut fa c ile m e n t d ete rm in e r le c a r a c t e r e fonctio nn el tie I ou de К. S i on pose qu'une e x p re s s io n e t sa r é c r it u r e appar- tie n n e n t a la méme c a t é g o r ie , d is o n so c , comme I x — > x, Kxy — >x, i l v ie n t :

oc( I x ) ^ ocX ocXKxy ) fly________

Focaf ffldďkxT________ ocx

FocFßaK

0 ' une manil*re com parable, on o b tie n t ľ e x p re s s io n FFccF0jFFctßF<x|-S. En d ésig n an t par (F X ) ľ e x p ressio n a t t r ib u a n t ё X un c a r a c tô r e f o n c tio n n e l, on a done: ( F I ) Focal ( Г К ) FocFßaK ( F S ) FftxFßjl faßfo<|S.

C u rry a form ule e t démontré un théorém e, d i t "de c o n s tr u c tio n du s u j e t " , qui in té r e s s e nos in v e s t ig a t io n s . I I donne une t e c h n i­ que perm etia.nt ď o b t e n ir la d ed u ction par ( F ) du caractfere fo n c ­ tio n n e l (q u ’ i l n 'e s t pas b eso in de c o n n a ltre avan t de ľ e n t r e - p re n d re ) ď u n com binateur donne X, b p a r t i r de prem isses données, ou ď é t a b l i r que la d e d u ctio n ď u n c a r a c t e r e fo n c tio n n e l pour X e s t im p o ssib le dans le systéme c o n s id é ré . Nous le p ré s e n te ro n s moins form ellem ent e t en le r e s t r e ig n a n t ď a b o rd á un cas s im p le . P u is , nous in d iq u e ro n s comment i l e s t p o s s ib le de le g e n e r a lis e r pour r e tro u v e r l'e n s e m b le des cas du théoreme de C u rry .

S o it á d é d u ire l e c a r a c t e r e fo n c tio n n e l d 'u n com binateur X par ( F ) a p a r t i r de (F K ) ( F S ) donnés comme schémas d'axiom es e t en se bornant a u t i l i s e r le s term es p r i m i t i f s K e t S . Notons que, comme to u te s le s m étafo rm u les, (F K ) ( F S ) in c o rp o re n t en soroine la r é g le de s u b s t it u t io n dans le u r fo rm u la tio n . Chaque v a r ia b le a , ß , . . .

peut done é tr e rem placée par des symboles quelconques de ca teg o ­ r i e s . Nous a p p e lle ro n s J ^ ce systéme fo rrael.

X e s t évidemment une m olecule composée de К et de S par ap­ p lic a t io n . On prouve a lo r s le théuréme s u iv a n t:

S i on peut d éd uire des schemas d'axiom es (F K ) ( F S ) , par ( F ) , le c a r a c té re fo n c tio n n e l d'un com binateur X, s o it i}X , a lo r s ( П i l e x is ie une d ed uction normale de t jX á p a r t i r de (F K ) ( F S ) , par ( F ) . C e tte d ed uction e s t t e i l e q u 'i l e x is te des termes X j, X(J,

... T)q pour le s q u e ls e i l e o b tie n t le s énoncés TqXq, c .- á - d . X^ a le c a r a c te r e fo n c tio n n e l т)р e t c . ;

( Ц ) X j, Xq forme une c o n s tru c tio n normale de X á p a r t i r de K, S par a p p lic a t io n . C e tte c o n s tru c tio n e s t unique;

( I I I ) s i Xk n 'e s t n i K n i S, c .- á - d . s ' i l a la forme * i Xj> a lo r s i) j : c a r a c te re fo n c tio n n e l de X^ s 'o b t ie n t en p la ę a n t F devant le c a r a c te re fo n c tio n n e l de X^ s u iv i du c a r a c té re fo n c tio n n e l de Xk ) ; (I_V) s i Xk e s t K ou S, a lo r s *)kXk e st une in s ta n c e de (F K ) ou de ( F S ) ;

(^ ) s i X ne comporte pas K (re s p e c tiv e m e n t, ne comporte pas

S ) , a lo r s aucune in s ta n c e de ( F S ) (ro s p e c tiv e m o n t, de ( F # ) ) n'm- t e r v ie n t dans la d ed uction normale de X.

En e s q u is s e , la preuve e s t la s u iv a n te : de méme que s i Xk e st obtenu par a p p lic a t io n de Xj e t do Xj, i l e x is te une c o n s tru ­ c t io n par a p p lic a t io n , de forme 4u i e s t la c o n s tru c tio n

I J

d it e "norm ale" de Xk , dé méme s i e s t obtenu par ( F ) de t j^X^ e t de ’’J j X j . i l e x is te une d ed uction par ( F ) de forme

v > . . ? Л .

qui e s t la d ed uction nurmale de f ) kXk . O’ a u tre p a r t , c e t t e deduc­ tio n normale s 'e f f e c t u e fen somme sur une c o n s tru c tio n normale puis­ que la d éd uction normale de T) k Xk se confond avec la c o n s tru c tio n normale de Xk quand le s t) ne sont pas c o n s id é ré s . C ela lé g itim e О ) e t ( П ) . On é t a b l i t ( I I I ) en remarquant que pour o b te n ir par (K ) i l ta u t qu'on a i t et ^ t e l s que i j i * = i l )jQ k - I I v ie n t a lo rs:

( I V ) e t (V J sont a peu prés é v id e n ts á p a r t i r de ce qui p re ­ cede. En p r a tiq u e :

Pour ch erch e r a d é d u ire (F X ) de (F K ) ( F S ) , on procede a i n s i : ( I ) on se donne la c o n s tr u c tio n normale de X; p. e x ., s i X e s t SK

— зк^~К ’ ^ pour chaque Xk de c e t t e c o n s tr u c tio n qui n 'e s t n i K n i S, i c i 3. SK, on p la c e devant sa m ajeure, i c i le S de 1. 5, un r) de forme f 1) ^ ’ *)j f ig u r e I е c a r a c t é r e fo n c ­ tio n n e l de sa mineure e t t). c e lu i de le u r c o n c lu s io n , selo n ( I I I ) . On a i c i т) j s on а* * г *Ьие aux X^ de c e t t e con­ s t r u c t io n qui sont K ou S le r) donne re sp e ctive m e n t par (F K ) et par ( F S ) . I c i T)t = F Fqí F <3 j F F oí p Fci y-, - FaF|3oc, (4 ) pour chaque Xj qui e s t ä la f o is la majeure ď u n com binateur Xk m o lé c u la ire , e t id e n tiq u e ä K ou ä S , on a done d if f é r e n t s rj , (5 ) on examine a lo r s en t i r a n t to u tes le s consequences des é g a lit é s s i la posses- aio n de ces d if f é r e n t s i) e s t co m p a tib le . E l l e ne ľ e s t pas s i 1' a n a ly s e a b o u tit ä des a b s u rd ité s (p . ex. ä i d e n t i f i e r a ä Fotß). Aucun c a r a c t é r e fo n c tio n n e l n 'e s t done d e d u c tib le pour X. E l l e e st com p atib le dans le cas c o n t r a ir e , la d ed u ctio n de i)X e s t pos­ s ib le e t la preuve de c o m p a t ib ilit y en f o u r n it le rtiodéle. I I e st c l a i r dans ľ e x e m p le que J - 01, de la i] t = FFaF|30<FFo<(3Faa. Ona:

F F a F Qg F Fi<*GF ot a S ________• Fa FQcxK F FaßFaoc( SK)

Ce théoréme peut é t r e form ule p lu s généralem ent: i l demeure v r a i pour le s d ed u ctio n s par ( F ) depuis to u t ensemble de prem isses a u tre s que (F K ) ( F S ) expnm ant le c a r a c t é r e fo n c tio n n e l d 'u n en­ semble de termes p r i m i t i f s t j ... t^ . I I s u f f i t do rem placer dans sa fo rm u la tio n e t dans sa preuve K, S par t p . . . , t^ , (F K ) ( F S ) par ( F 11) , . . . , ( F t p ) . I I demeuru v r a i ’ égalem ent s i le s termes dont le s schemas ď a x io m e s donnent le c a r a c t é r e fo n c tio n n e l ne sont pas des p r i m i t i f s (p . ex. s i ( F I ) e s t a jo u té a (F K ) ( F S ) dans un langage ou K e t S seulem ent sont des p r i m i t i f s ) , dés 1огз que la c o n s tr u c tio n de X e s t unique. Nous aurons ä f a i r e usage de ce théoréme mais c 'e s t un a u tre r é s u l t a t de C u rry qui In t e r e s s e p lu s d i rectem ent n o tre p ro b lé m a tiq u e .

S i aux schemas ď axiomes (F K ) ( F S ) on a p p liq u e la tra n sfo rm a ­ tio n T s u iv a n te : on rem place F par P (q u i note ľ im p lic a t io n e t en é c r it u r e p r é f ix é e ) e t on supprime le s u j e t , c .- ä - d . le

combi-n ateu r ecombi-n q u e stio combi-n , on o b tie n t r e s p e c t ivement: (1) RxPßa (2) P P a Pß^PPaßPay. Par la méme tra n sfo rm a tio n T, la ré g le ( F ) d e vie n t qui e s t la ré g le ( P ) tíe modus ponens. Or, on s a it que ( l ) e t ( 2 ) forment avec ( P ) un ensemble de schemas d'axiom es eomplet pour le c a lc u l p ro p o s itio n n e l in t u it i o n n is t e 1 de ľ im p lic a t io n pure (c .- á - d . sans n e g a tio n ). Nous d iro n s en b re f "a x io ro a tise n t Э ", I I s 'e n s u it par re c u rre n ce q u 'a to u te these de correspond par T une these de ] , et que, en ap p elant (P X ) la form ule qui correspond par T á ( F X ) , s i (F Z ) e s t d e d u c tib le par ( F ) de deux prem isses ( F X K F Y ) , a lo r s (P Z ) e st d e d u c tib le par ( P ) de ( P X ) ( P V ) .

On peut done se demander si le s schemas d'axiumes qui c a r a c t é r is e - r a ie n t fo n c tio n n e lle m e n t le s com binateurs d'une base quelconque cor­ respondent de la méme mani é re , c.- á - d . par 1, ä un ensemble com- p le t do schemas d'axiom es pour 3 . C urry in d iq u e seulement que pour le s bases connues { K, W, С, в| e t | к , W, В'} , dont chaque combina- teur posséde dans J j un c a r a c te re f o n c tio n n e l, T o b tie n t comme pour { k , s } un t e l ensemble. En a lla n t un peu p lu s lo in , nous demontrerons le theor ems s u iv a n t:

S o it un ensemble de com binateurs { X j , . . . , Xffl J dont chacun pos­ séde dans Tj (ou {k, s } e s t une b ase) un d é f in is s a n t X' ^, . . . , X 'm, re s p e c tiv e m e n t, ayant un c a r a c te re fo n c tio n n e l, c .- á - d . t e l qu'on a i t t) г X' 4, . . . . t,|nX ' n). S o it i ) aK e t n^S le s e x p ressio n s (F K ) ( F S ) . Les form ules ( P X 1. ) , . . . , ( P X obtenues en a p p liq u a n t T

t P F

a X p s o it en b re f . . . , tj^, a x io m a tis e n t 3 s i e t seulem ent s i dans le systéme _c dont X ,, . . . . X _{l w fn} sont le s s e u ls p r i m i t i f s e t •••» s e u ls schemas d'axiom es

(1 ) i l e x is te des com binaisons de X j, . . . , Xm, d iso n s Qt e t Ll^, t e l i e s que ^ Q j , T)bQ2

(2 ) T)aQ j, T)bQ2 se déd uisent par ( F ) de O jX p . . . , t)mXm (ou se confondent avec t ^ X j ou avec i)2X2... ou avec T)fflXm s i ľ un des X^... Xm e s t K ou S ) .

S i ( 1 ) e t (2 ) sont v r a i s , en e f f e t , comme á to u te d ed uction s 'e f f e c t u a n t sur des form ules de J j ou sur des form ules de Í - , i l correspond une d ed uction s 'e f f e c t u a n t sur le s form ules qui le u r

P P

correspondent par T, t) ...t i se d éd uisent des schémas d 'a x io

-P P P P

mes » Л . s l i s ne se confondent pas avec eux, e t \)r i) se de'duísent

/ P p a , o i

eux. Les deux systém es sont done d é d u c tiveroent e q u iv a le n ts . Comme le prem ier a x io m a tise 3, le second égalem ent.

p Montrons que, récip ro q u em en t, s i C P X' ^ >... ( px' ro^> s c il', : i')i>

ax io m a tisen t 3, a lo r s ( I ) e t (2 ) sont v r a i s . Supposons

* p p , p p p

d 'a h o rd que chaque r, , . . . , ij m e s t d if f e r e n t de % Comme i} a ,

ax io m a tisen t 3, e t comme par hypothése également,

le s deux systém es sont deductivem ent e q u iv a le n ts . Or, s i dans

P P Р Р

chaque form ule d'une d ed uction qui o b tie n t t j , T) b de ... on rem place P par F e t s i on a p p liq u e t ). , . . . , q m resp e ctive m e n t á X j, . . . , Xm, ce qui forme t ) j X j ... T)mXm1 on o b tie n d ra par ^ ^ T) a ® ľ ^b^2‘ ° “ ®1* ^2 50nt ^es com binaisons de X1 , . . . , X^. En e f f e t , chaque d ed uction par ( P ) e s t a in s i tran sform ée en une de­ d u ctio n par ( F ) , le remplacement de P par F d eterm in an t une formule unique e t le s u je t de l a c o n c lu sio n é ta n t déterm iné de m aniere u n i­ que par ceux des p rem isse s, Supposons m aintenant q u 'i l у a i t un

P P P

T). ₁ ( l = I . . . m) _{^ ^} qui se confonde avec n ₃ ou avec t) ₀ e t s o it X,₁ le s u je t a t t r ib u e a , a lo r s (1) e t (2) sont v r a is c a r oil Qj = K, ou b ien ^h 02’ 011 ^2 = ^ se соп* оп^ avec Done, s i le s form ules ( P X ' j ) , ( P X 'm) , obtenues comme in d iq u é , axioma-t is e r iaxioma-t 3, а1огз ( I ) e t (2 ) sont v r a i s .

Notons que ( I ) r e v ie n t a e x ig e r q u 'i l у a i t dans 7.^ deux com­ b in a te u rs OŁ , Q2 ayant le s c a r a c t e r e s fo n c tio n n e ls de К e t de S, re s p e ctiv e m e n t, e t non pas que s o it un d é f in is s a n t de K, C)2 un d é f in is s a n t de S. Comme le remarque C u rry , en e f f e t , sur exemple, deu* com binateurb peuvent a v o ir le méme c a r a c t é r e f o n c t io n n e l, cororoe Uj e t K, Q2 e t S , sans a v o ir la méme r é g le de r é c r i t u r e . On peut démontrer t o u t e f o is :

C o r o lla ! r e ; s o it { X j , . . . , X(nj , ( P X ' ^) , . . . , comme dans le théoréme p ré c é d e n t, mais ou, en o u tre , | X p Xm | e s t une base. ( P X ' j ) , ( P X 'm) ax io m a tise 3 s i ( a ) : le s form ules T, aK' , T)bS ' , oil K' e t S ' sont des d é f in is s a n t s dans 7,^ de К e t de

S re s p e c tiv e m e n t, se d éd u isen t par ( F ) de T)^X^, . . . , т)т Хт , ä moins que T)aK, t jöS ne f ig u r e n t parmi т ц Х р . . . , i ) raXm.

En e f f e t , s i ( a ) e s t v r a i , a lo r s (1 ) e t ( 2 ) sont v r a i s , K' et S ' é ta n t des com binaisons de X . , . . . , X : _{L m} done ( P X ' , ) , . . . , (PX' )_{L * m} a x io m a tise n t 3. En revan ch e, la c o n d itio n ( a ) n 'e s t pas nécessaire ca r s i ( P X ' j ) , . . . , (P X ' ) a x io m a tis e n t 3 a lo r s ( l ) e t ( 2 ) sont

v r a i s , selo n le théoreme p rece d e n t, mais ( l ) e t (2) n 'im p liq u e n t pas ( a ) , le s com binateurs Qt , pouvant ne pas e tr e к ' , S ' .

On a jo u te ra que s i un ensemble de form ules axioma-t is e n axioma-t 3, a lo r s pour le s e x p ression s rj^, . . * . т ) р obtenues en rem- p la ę a n t P par F dans M p , i l n 'e x is t e pas to u jo u rs un en­ semble de com binateurs X p Xp t e ls que pour le u r s d é fin is -sa n ts X ' p . . . , X 'p dans on a i t ^ p ^ ’ p* e t t e l3 4^e X j, . . . , Xp forment une base.

Nous nous co n ten tero n s de remarquer q u 'on c o n n a lt pour 3 des systém es ä un seu l schéma ď axiome e t qu'aucune base n 'a qu'un seul élém ent.

Nous term inerons en c o n s tr u is a n t ä p a r t i r du c o r o l l a i r e précé- dent e t d'une base de com binateurs d é jä donnée un ensemble de for- mules qui a x io m a tisen t D. Ľ exemple sera sim ple pour i l l u s t r e r seulement la méthode.

S o it j e , A, s } avec Axy — > y. On a é t a b li p lu s haut que ( c , A, s j e s t une base e t q u 'e lle permet d 'o b t e n ir К = ^^ CA. O 'a u tre p a r t , dans J p A = tjf K (SK K ) ; en e f f e t : K (SKK )xy —»-SKKy * Ky (Ky ) — * y . Or, on peut d ed u ire dan9 ip- FaF|3|3(K(SKK)), c a r d'une p a rt on a Fo o (S K K ), comme C urry ľ é t a b l i t p. 2Ö5, (it done:

l.FFflflFg FflQ K _____________2 ._Ff3j3 (SKK ) Й Г (З А (К (5 К К Г '

ou 1. p st (F K ) avec U = F0ß , /3 = « , e t 2. e s t (F ( S K K ) ) avec a - ß . On a au ssi oans J t FFaFßyFßFajC ( c f . p. 279).

O 'a u tre p a r t , la form ule i ) aK' , c .- á - d . F«F(30t(CA), se d éd uit par ( F ) dans ? 2 qui posséde le s p r i m i t i f s C, A, S e t le s schémas d'axiom es s u iv a n ts :

(F C ) FFaFPf F/3FajC, (F A ) KxFflßA,

(F S ) FFctFßf FFaf3 F a y S .

I I v ie n t en e f f e t en u t i l i s a n t le théoreme de c o n s tru c tio n du s u j e t :

1. FFORxOtFotFOOtC 2. FQFactA 3. FotFpa(CA)

oú l . e s t (F C ) avec oí , p=oc , y = oí , e t 2. e s t (F A ) avec a =P> , p = a .

РР«Р|ЗуР|ЗРо<

J

PotPpß

PPaPOjPPotflPa j

ax io m atise 3. Rappeions q u 'i l s u f f i t d 'a jo u t e r le schéma d'axiom e PPPaO aa ä une a x io m a tis a tio n tie 3 , p. ex. ä c e l i e qui p récéd e, pour a x io m a tis e r le c a lc u l c la s s iq u e ď im p lic a t io n .

En u t i l i s a n t le s théorémes p o rta n t sur ce qui e s t nommé " l a s t r a t i f i c a t i o n " , dont nous n 'a vo n s pas pu t r a i t e r , on o b t ie n d r a it des r é s u lt a t s p lu s é lé g a n ts e t p lu s f o r t s .

C e tte m aniere d 'o b t e n ir la n o tio n P e t ses p r o p r ié té s dans 3, en p lu s de son u t i l i t é tech n iq u e , i l l u s t r e b ien le f a i t qu'une p a r t ie du t r a v a i l mathématique c o n s is te á a t t e in d r e des n o tio n s d it e s "de b ase" dans une c e r t a in e th é o r ie au terme ď u n p arco u rs p lu s ou moins long e f f e c t u é avec le s moyens d*une a u tr e . I I re s te - r a i t i c i b comprendre ce qui permet a F d 'e t r e une s o rte de gene­ r a l i s a t i o n de P. Ce s e r a i t 1* o b je t d'un e a u tre etude..

U n iv e r s it é Lyon I I I France

Je a n - P ie r r e G i n i s t i

TWORZENIE POJĘĆ W LOGICE K0MBINAT0RYC7NEJ

Przedmiotem p ra c y j e s t lo g ik a ko m b inatoryc2n a , g a łą ź l o g ik i u- fundowaria przez ta k ic h autorów , ja k S c h ö n fin k e l i C u rry , k t ó r e j n a jb a r d z ie j znaczącą cechą j e s t tw orzenie języków form alnych po­ zbawionych zmiennych. U pierwszym rz ę d z ie p rz e d sta w ia s ię p o ję c ia bazowe tego p r z e d s ię w z ię c ia ,

t j.

t e o r ię kombinatorów

i

t e o r ię fu n ­ k c jo n a ln o ś c i. Podejm ując i ko n tyn u u jąc r e z u lt a t y , j a k ie o s ią g n ą ł C u rry , a u to r poddaje a n a li z ie sposób, w j a k i można otrzym ać z u p e ł­ ny z b ió r aksjomatów d la rachunku zdaniowego i n t u i c

jonistycznego

, wy­ chodząc od u tw orzen ia zupełnego zb io ru kombinatorów p ie rw o tn y ch .