mod Ex03c

incl Mtex

incl Mtexln

incl Maux

loc rem 
  \para \bf  3. CVIČENIE Z PREDMETU 1-AIN-470 ŠPECIFIKÁCIA A VERIFIKÁCIA 
  PROGRAMOV  \end 

loc rem 
  \para* \it  Meno:  \end 
  \para* \it  Verzia CL:  \end 5.81.21.2 
  \para* \it  Dátum:  \end pondelok 27.2.2023 
  \para* \it  WWW:  \end 
  http://www.ii.fmph.uniba.sk/cl/view.php/courses/1-AIN-470-svp/2223ls/?lang=sk 
  \para* \it  Kontakt:  \end Jan.Komara(at)fmph.uniba.sk 

loc rem 
  \para \bf  Úvodná poznámka.  \end Toto cvičenie je venované týmto 
  témam: 
  \items 
   \item \para celočíselná odmocnina (názorný príklad), 
   \item \para Cantorova párovacia funkcia a aritmetizácia karteziánskeho 
         súčinu, 
   \item \para Catalanova párovacia funkcia. 
  \end
  \para Zadanie sa skladá z týchto súborov: 
  \items 
   \item \para Súbory \it  mtex*.cl  \end obsahujú makrá pre CL-TeX. 
   \item \para Súbory \it  maux*.cl  \end obsahujú definície a vlastnosti 
         pomocných funkcií a predikátov. 
   \item \para Súbory \it  ex*.cl  \end obsahujú úlohy, ktoré máte riešiť 
         na tomto cvičení. 
   \item \para Súbor \it  msyntax.cl  \end obsahuje základnú syntax systému 
         CL. 
  \end
  \para Tieto súbory sa musia skompilovať v správnom poradí. Presný postup 
  je uvedený v súbore \it  readme.txt  \end. 

loc rem 
  \para \bf  Hodnotenie.  \end 
  \items 
   \item \para Počet bodov za úlohy v tomto súbore: 0 
   \item \para Počet bodov za prémiove úlohy v tomto súbore: 4 
  \end
  \para Odovzdať do 4.3.2023 (sobota). 

loc rem 
  ******************************************************************************
  ********************************* EXERCISES **********************************
  ******************************************************************************

rem 
  \para \bf  Literature.  \end 
  \items 
   \item \para \it  [1]  \end J. Komara. Specification and Verification of 
         Programs. Online. 
   \item \para \it  [2]  \end Ján Kľuka. Úvod do deklaratívneho 
         programovania. Online. 
   \item \para \it  [3]  \end Ján Komara. Recursive Functions. Online. 
  \end

rem 
  \para \bf  [CL] Remark.  \end Catalan pairing function - see the module \it  
  Maux*  \end. 

rem 
  \para \bf  Chapter. Programs Operating on Lists.  \end 

rem 
  \para \bf  Section. Operations on Lists.  \end 

rem 
  \para \bf  Counting the number of occurrences in lists.  \end 

fun/2 Count 'Tex_f2_ln_count'
  Count(a,0) = 0
  Count(a,x,xs) = Eqf(a,x)+Count(a,xs)

rem 
  \para \bf  Union list.  \end 

fun Union 'Tex_f1_ln_union'
  Union(0) = 0
  Union(xs,xss) = xs++Union(xss)

rem 
  \para \bf  Section. Combinatorial Functions over Lists.  \end 

rem 
  \para \bf  Permutations.  \end 

pred/2 Perm 'Tex_p2_ln_perm'
  Perm(xs,ys) <-> \a a Count(a,xs) = Count(a,ys)

rem 
  \para \header* pred/3 Inserted 'Tex_p3_ln_inserted' \end We have 
  \eq* 
    Perm(ys,0) <-> ys = 0
  \end
  \eq* 
    Perm(ys,x,xs) <-> \e zs(Perm(zs,xs) & Inserted(ys,zs,x))
  \end
  \para where 
  \eq* 
    Inserted(ys,xs,a) <-> \e zs1\e zs2(xs = zs1++zs2 & ys = zs1++(a,zs2))
  \end

rem 
  \para \bf  Generating permutations. \it  (2 bonus points)  \end  \end Define 
  the function \ft Perms(x) \end such that 
  \eq* 
    ys in Perms(xs) <-> Perm(ys,xs)
  \end
  \para \it  Hint.  \end \header* pred/3 Inserted 'Tex_p3_ln_inserted' \end 
  \header* fun/2 Mape  \end \header* fun/2 Interleave  \end 
  \header* fun/2 Mapi  \end First define auxiliary functions 
  \ft Mape(a,xss) \end, \ft Interleave(a,xs) \end and \ft Mapi(a,xss) \end such 
  that 
  \eq* 
    ys in Mape(a,xss) <-> \e zs(xs in xss & ys = a,zs)
  \end
  \eq* 
    ys in Interleave(a,xs) <-> Inserted(ys,xs,a)
  \end
  \eq* 
    ys in Mapi(a,xss) <-> \e zs(zs in xss & Inserted(ys,zs,a))
  \end

fun/2 Mape 
  Mape(a,xss) = Foo

fun/2 Interleave 
  Interleave(a,xs) = Foo

fun/2 Mapi 
  Mapi(a,xss) = Foo

fun Perms 
  Perms(xs) = Foo

rem 
  \para \bf  List partitions.  \end 

pred/2 Concp 'Tex_p2_ln_concp'
  Concp(yss,xs) <-> Union(yss) = xs & 0 !in yss

rem 
  \para We have 
  \eq* 
    Concp(yss,0) <-> yss = 0
  \end
  \eq* 
    Concp(yss,x,xs) <-> 
    \e zss(Concp(zss,xs) & yss = (x,0),zss) \/ 
    \e zs\e zss(Concp((zs,zss),xs) & yss = (x,zs),zss)
  \end

rem 
  \para \bf  Generating list partitions. \it  (2 bonus points)  \end  \end 
  Define the function \ft Concps(xs) \end such that 
  \eq* 
    yss in Concps(xs) <-> Concp(yss,xs)
  \end
  \para \it  Hint.  \end \header* fun/2 Mapc1  \end \header* fun/2 Mapc2  \end 
  First define auxiliary functions \ft Mapc1(a,xsss) \end and 
  \ft Mapc2(a,xsss) \end such that 
  \eq* 
    yss in Mapc1(a,xsss) <-> \e zss(zss in xsss & yss = (a,0),zss)
  \end
  \eq* 
    yss in Mapc2(a,xsss) <-> \e zs\e zss(zs,zss in xsss & yss = (a,zs),zss)
  \end

fun/2 Mapc1 
  Mapc1(a,xsss) = Foo

fun/2 Mapc2 
  Mapc2(a,xsss) = Foo

fun Concps 
  Concps(xs) = Foo

