Taalblaat - Festschrift for Johan Jeuring

TAALBLAAT Festschrift for Johan Jeuring TAALBLAAT Festschrift for Johan Jeuring Taalblaat Festschrift for Johan Jeuring Preface This Festschrift celebrates Johan Jeuring’s 60th birthday and honors not only his contributions to computer science and education, but also the influence he has had on his friends and colleagues. Throughout his career, Johan has affected all of us in how we think about programming, education, and the intersection of theory and practice. The articles collected in this Festschrift reflect the breadth and depth of this influence. They are wonderfully varied in both style and content, ranging from personal anecdotes of Johan’s mentorship to rigorous mathematical proofs. Some authors share memories of collaboration and friendship, while others present new research inspired by Johan’s work in functional programming, generic programming, and educational technology. The cover image is inspired by the cover of Johan’s PhD thesis, which featured a staircase in black and white. The staircases on this cover represent the various research directions he has pursued throughout his career, which sometimes came together again. Regarding the color, many people could probably guess that Johan’s favorite color is red. Lastly, the palindrome title reflects one of Johan’s many interests. We hope that Johan will enjoy reading this Festschrift as much as we have enjoyed creating it. Each contribution reflects not only academic respect but also genuine appreciation for a colleague, mentor, and friend. July 2025 Alex Gerdes Hieke Keuning Wouter Swierstra Table of Contents On the Avoidance of Error ........................................... 1 Roland Backhouse Stepwise refinement with Dafny assistance ............................. 7 Lex Bijlsma “Nondeju, gij hoort HOERA” ......................................... 13 Maarten Fokkinga Agda-ventures with PolyP ........................................... 21 Jeremy Gibbons and Patrik Jansson Thank you Johan!................................................... 37 José Pedro Magalhães Incremental Optimal-Fit Line Breaking ................................ 39 Lambert Meertens Algorithmics for Unicians ............................................ 53 Steven Pemberton Pax et Bonum ...................................................... 61 Alberto Pettorossi Letters that are not just words ....................................... 63 Marc van Kreveld The end of the logic tools? ........................................... 67 Josje Lodder AI in Education .................................................... 77 Arno Siebes Refactoring a Researcher into CER: A Heuristic Algorithm for Disciplinary Realignment ............................................ 85 Isaac Alpizar-Chacon Bridging computer science and psychometrics ........................... 91 Matthieu J. S. Brinkhuis On Leadership ...................................................... 95 Ioanna Lykourentzou Preface V Semi times ......................................................... 97 Enrico Benedetti, Eduardo Carneiro de Oliveira, Aditya Joshi, Heleen Kerstholt, Jacco Krijnen, and Niek Mulleners Beyond the Classroom: Johan’s Pioneering Role in Scalable Communication Skills Education ...................................... 103 Marcell van Geest and Jordy van Dortmont The Jeuring Test.................................................... 105 Richta IJntema, Nicole Mastenbroek, Michiel Hulsbergen, Frans Grosfeld, Majanne Wolters, Jordy van Dortmont, Marcell van Geest, and Ignaz Kevenaar Johan’s educational biking tour ....................................... 117 Mirko Lukács On Student Steps, Learning Environments and Expert Feedback for Novice Programmers ................................................ 119 Natalie Kiesler and Dominic Lohr A Note of Appreciation for Johan Jeuring .............................. 131 Shriram Krishnamurthi Inspired by AI, built by humans ...................................... 133 Sylvia van Borkulo, Peter Boon, Wim van Velthoven, and Laura van der Lubbe Johan throughout the years .......................................... 135 Alex Gerdes, Hieke Keuning, and Wouter Swierstra On the Avoidance of Error Roland Backhouse[0000-0002-0140-8089] 1 Introduction I first met Johan Jeuring when he was an undergraduate in Groningen but I did not get to know him well until after he had completed his PhD thesis [Jeu93]. The first paragraph in his thesis is about the frustration he experienced as the result of an error in a mailer. When asked to submit an article for his festschrift my immediate thought was therefore to write something about the errors that I have encountered, and to include some brief comments about how to avoid error. There are lots of examples I could choose but I have limited the examples to two from my early career (in sections 2 and 3) and one quite recent example (section 4). The final section draws some conclusions on how to avoid error. 2 Conway’s Factor Matrix One of the first errors in the literature I remember very clearly is in Conway’s book [Con71] on Regular Algebra and Finite Machines. I was attracted to the book because of the word “Algebra” in the title; at the time, and still today, I felt that algebra was of vital importance to algorithm design, and regular algebra particularly so since it is the algebra of three components of all non-trivial algorithms: choice, sequencing and iteration. Conway’s book had a great influence on my PhD study; the importance of algebra is clearly a sentiment shared by Johan. I was particularly impressed by Conway’s theory of factors of a language. Theorem 4 of chapter six introduces the factor matrix of a regular language E. Denoting the entries of the matrix by Eij , and the left and right factors of Eby Liand Ri, the theorem is as follows. Each Eij is a factor, and each factor is one of the Eij . There exist unique indices l,rsuch that E=Lr=Rl=Eij and Li=Eli and Ri=Eir for each i. Hence the factors naturally form a square matrix among the entries of which is E. Immediately following the proof of this theorem, the following note is made: This organization of the factors as Eij does prevent Efrom occurring twice in its factor matrix, Unfortunately, there is an error in this sentence. Instead of saying “does prevent” the sentence should say “does not prevent”: there is a missing negation in the sentence! 2 Roland Backhouse I recall that I spent almost two days trying to understand why the theorem “does prevent Efrom occurring twice” before I changed tack and looked for an example of a language that does occur twice in its factor matrix. Indeed, such an example is easy to find. The language (aa)∗has (admissible1) factor matrix (aa)∗(aa)∗a (aa)∗a(aa)∗. There are two distinct entries in this matrix, (aa)∗and (aa)∗awhich both occur twice. Both are factors, and left factors, and right factors, of (aa)∗. So one is left wondering which are the “unique” indices land r mentioned in the theorem! There are indeed two options — the only requirement is that l=r(because (aa)∗is the repeated entry on the diagonal). In retrospect, it shouldn’t have taken me two days to spot the missing “not” in Conway’s note. Without the “not” the sentence sounds strange —at least to a native English speaker like myself— and the sentence ends and in general certain factors appear repeatedly. How I missed this I do not know. However, this simple error highlights a problem with Conway’s statement of the theorem. The theorem is correct so long as it is properly interpreted. The indices mentioned in the theorem are not arbitrary: in formal terms, the index given to the left factors is a function and the index given to the right factors is also a function, but these two functions must satisfy a couple of properties, one of which states how they are linked. The theorem assumes that these two functions are given; the claimed unicity properties are with respect to the given functions. (In fact, the index functions are an unnecessary complication: the theorem can be formulated in a way that avoids them altogether.) 3 Quadratic Collision Handling Another example of an error that took me a long time to resolve was concerned with hashing techniques. In my first lecturing post in the 1970s, I had to lecture on data structures. Since I had not previously studied hashing techniques, I learnt about them by studying the textbook that had been recommended by my predecessor on the course. With regard to quadratic collision handling, the following assertion was made: When the table size is a power of two, only half the table is searched. 1In almost all cases, both ∅and T∗are factors and left and right factors of a language Eover the alphabet T; in this case, the factor matrix is 4×4, and not 2×2, with entries ∅and a∗appearing repeatedly. In practical applications these entries are deemed “inadmissible” in the sense that they can be ignored. They have been omitted here for simplicity. Stepwise refinement with Dafny assistance 9 { queens := {}; var columnsSearched := 0; while columnsSearched < 8 decreases 9 - columnsSearched invariant ∀queen :Position | queen ∈queens :: Valid ( queen ) invariant ∀queen1:Position , queen2 :Position | queen1 ∈queens ∧queen2 ∈queens ∧queen1 =queen2 :: ¬Threatens ( queen1 , queen2 ) { var found :Position; found := NewSafePosition ( queens , columnsSearched ); assert columnsSearched < Column ( found ); if Valid ( found ) { assert IsSafePosition ( queens , found ); assert ∀queen :Position | queen ∈queens :: ¬Threatens ( queen , found ); queens := queens + { found }; } columnsSearched := Column ( found ); } } For convenience’ sake, we have introduced the abbreviation function Column ( pos :Position):nat { match pos case Coordinates (hor , vert ) ⇒hor } More importantly, we have postponed both the test of whether a position is safe and the task of finding one to the next refinement step, merely specifying: predicate IsSafePosition ( queens :set <Position >, pos :Position) requires ∀k|k∈queens :: Valid (k) ensures IsSafePosition (queens , pos ) =∀k|k∈queens :: ¬Threatens (k , pos) method NewSafePosition ( queens :set <Position >, columnsSearched:nat) returns ( found :Position) requires ∀k|k∈queens :: Valid (k) requires 0 ≤columnsSearched < 8 ensures Valid ( found ) =⇒IsSafePosition ( queens , found ) ensures columnsSearched < Column ( found ) Again, all is verified. Again this indicates mere well-formedness for the last specifications, but this time it also tells us the columnwise approach to the implemen- 10 Lex Bijlsma tation of PlaceAllQueens will succeed if we manage to come up with the next refinements. 4 Third version Let us start with the safety test, as that is entirely straightforward: merely a trivial copy of the specification! predicate IsSafePosition ( queens :set <Position >, pos :Position) requires ∀k|k∈queens :: Valid (k) ensures IsSafePosition (queens , pos ) =∀k|k∈queens :: ¬Threatens (k , pos) { ∀k|k∈queens :: ¬Threatens (k, pos) } But finding a safe position requires more work, although it is only a matter of sequentially checking squares. method NewSafePosition ( queens :set <Position >, columnsSearched:nat) returns ( found :Position) requires ∀k|k∈queens :: Valid (k) requires 0 ≤columnsSearched < 8 ensures Valid ( found ) =⇒IsSafePosition ( queens , found ) ensures columnsSearched < Column ( found ) { var nextcolumn := columnsSearched + 1; while nextcolumn ≤8 invariant columnsSearched < nextcolumn ≤9 decreases 9 - nextcolumn { var nextrow := 1; // arbitrary while nextrow ≤8 decreases 9 - nextrow { var nextTry := Coordinates ( nextcolumn , nextrow ); if IsSafePosition ( queens , nextTry ) { found := nextTry; return; } else { nextrow := nextrow + 1;} } if nextcolumn =9 { nextcolumn := nextcolumn + 1;} } // if nextcolumn =9 { found := Coordinates (9, 9);} Stepwise refinement with Dafny assistance 11 } The assignment found := Coordinates (9, 9); is only there to signal the absence of a solution in the remaining columns (the value 9 acting as a sentinel). Again, this verifies and there are now no unimplemented specifications left. The initialization of nextrow in the inner loop is arbitrary; for finding all safe configurations other possibilities here should be tried as well. 5 Testing The Dafny verifier ensures that method PlaceAllQueens returns a set of positions that is safe, i.e. mutually non-threatening. What it does not guarantee is that this set’s cardinality will be 8, in other words, that we have succeeded in placing a queen in every column. So let’s run the program and see what results. The positions found by the current version are (1,1),(2,3),(3,5),(4,2),(5,4) But after these five placements we are stuck: obviously the queen for column 6 cannot be placed in any of the rows 1..5 (threatened horizontally); but (6, 6) is threatened diagonally by (1,1), (6,7) by (2, 3) and (6,8) by (3, 5). Clearly the number of queens placed is much dependent on the order in which the safe places are selected, and the Dafny specifications offer no help here. The classical treatment of the problem [4] does not have any suggestions on the most advantageous order either, except trying everything by recursive backtracking. And even that approach does not enable us to assert a postcondition |queens| =8, for we do not know a priori that such a solution exists. 6 Conclusion If we compare this process to the presentation originally given [4], there are two major differences. In the first place, the original treatment does not specify the steps postponed to the next refinement, but describes their actions in a kind of informal pseudocode – which does not lead to a reliable proof. Dafny, on the other hand, provides a proved program. In the second place, traditionally there is no feedback during the process, and feedback can only be provided by testing once the code is complete. Dafny, on the other hand, checks whether the use of as yet unimplemented steps is consistent with their specifications. In both these aspects, the assistance provided by Dafny is a big help in preventing mistakes. However, the specifications offer no help in finding the most productive order in which to consider possible placements, nor in proving that an eight-queen solution exists. 12 Lex Bijlsma References 1. Dijkstra, E.W.: EWD316: A short introduction to the art of programming (1971), circulated privately, available from the EWD Archive at the University of Texas 2. Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348–370. Springer (2010) 3. Leino, K.R.M.: Program Proofs. MIT Press (2023) 4. Wirth, N.: Program development by stepwise refinement. Communications of the ACM 14, 221–227 (1971) “Nondeju, gij hoort HOERA” Maarten Fokkinga → - ↑ u ← u ← - ↑ j → n → i → e ↓ u ← - ↓ u ↑ r ↑ i ← n ↓ j → r → - ↓ g ↓ g ← J ← t ↑ r ↑ j → n ↑ r ↑ j → i → e → u ↓ g ← - ↑ e ← n ↑ u ← n ↓ e ↓ t ← r ↑ j ↑ i → e ↓ t ↓ t ← i ↑ i → - ↑ g → - ← n ↓ u → g ↑ n ← u ↓ g ← - ↓ j ← - ↑ t → r ↑ i ↑ t → g → n ↓ n ↓ - ↓ J ← i ← i ← r ↑ j ↑ e ← r ↑ t ↑ g → n → n → u → u ↓ - ↓ J ↓ i ← r ← t ↑ g ↑ g → J ↓ i ↓ i ↓ r ↓ r ← t ← g ← j ↑ e ↑ e → J → i ↑ i ↑ - ← u ← n ← u ← n ↓ J → i → i → r → r ↑ - ↑ n ← n ← J 1 HOERA Beste Johan, op 12 augustus 2025 heb ik luidkeels Hiep Hiep Hoera gezongen. Dat geluid had je vast niet verwacht uit het verre oosten, maar je had het het kunnen horen als je goed geluisterd had! Proficiat met je zestigste verjaardag. Het is alweer lang geleden dat wij gedurende drie jaar op één kamer zaten. Beiden werkten we aan onze dissertatie. Jij als jong broekie, net afgestudeerd, en ik al in het midden van mijn loopbaan. Ik heb toen geen leeftijdsverschil tussen ons ervaren, terwijl ik nu al bijna twaalf jaar pensionado ben en jij nog zeven jaar “mag” voordat je de AOW leeftijd bereikt. Wat hebben we daar zitten kriebelen (squiggling). En met succes. Een HOERA was ook na afloop van die periode duidelijk te horen: voltooing van onze proefschriften. Ik denk met véél plezier terug aan die tijd. 2 HOERA Bij een verjaardag hoort een presentje. Deze puzzel wil ik je graag geven: Er zijn tien stukken jt_Jeuring en twee lege plekken, omgeven door een vaste rand. Een stuk kan verschoven worden (een “zet”) als er een passend lege plek naast zit. Stuk Jis iets dunner dan de andere stukken, en kan door een gleuf midden onderin uit het bord geschoven worden. De opgave is in zo min mogelijk zetten het stuk Jmidden onderin te krijgen – en dan uit het bord te schuiven. 14 Maarten Fokkinga Misschien vind je het presentje helemaal niet leuk; je bent er dagen mee zoet en wat voor nuttigs heb je bereikt als stuk Jer uit is? Mijn eigen pogingen mislukten; na een twintigtal zetten wist ik niet meer of ik in een situatie kwam die ik al eerder gehad heb. Spoiler: er zijn 112 zetten nodig. Maar –en nu hoor ik jou al Hoera roepen– de oplossing heb je al gezien! 3 HOERA Ik heb me lang afgevraagd hoe de oplossing voor deze puzzel geprogrammeerd kan worden. Heb je daar zelf al een idee voor? Ik vond het zó verrassend eenvoudig dat ik, nonjedu, hardop Hoera riep. Dat heb je misschien wel gehoord! Een programma dat een kortste pad in een graaf berekent, kan gebruikt worden om deze puzzel op te lossen. Een knoop in de graaf is dan een configuratie van de puzzel (de posities van de stukken op het bord), en een transitie in de graaf is een zet in de puzzel (het verschuiven van een stuk: een overgang van de ene configuratie naar een andere). De beginsituatie is de startknoop; iedere configuratie waarin stuk Jmidden onderaan staat, is een doelknoop. Omdat in de puzzel iedere zet omkeerbaar is, zijn de kanten in de graaf ongericht, en omdat iedere zet even zwaar telt, zijn de kanten gewichtloos. Een kortste pad in deze graaf, van de startknoop naar een doelknoop, geeft de oplossing voor de puzzel: de kortste zettenreeks van beginconfiguratie naar een doelconfiguratie! Een verschil met gangbare formuleringen van “het kortste pad in een graaf” is dat de knopen van de graaf niet bij voorbaat gegeven zijn, maar gedurende de berekening beetje bij beetje gegenereerd worden, steeds wanneer van een knoop de mogelijke zetten opgevraagd worden; dit impliceert dat de graaf samenhangend is. Ik wil je graag een Haskell programma hiervoor als presentje aanbieden. Bovendien –hoera– kunnen vele puzzels met deze aanpak opgelost worden: al díe puzzels waarbij er sprake is van “zetten” die de ene “configuratie” overvoeren in een andere, en het de bedoeling is een kortste zettenreeks te vinden die van een gegeven beginconfiguratie gaat naar een gewenste eindconfiguratie. Denk bijvoorbeeld aan deze puzzels: Torens van Hanoi, de ‘1-15 schuifpuzzel’ waarin stukken met de getallen 1-15 via één lege plek op volgorde geschoven moeten worden, de puzzel waarbij auto’s orthogonaal op een veld staan en alleen maar in hun lengterichting geschoven kunnen worden en “de rode auto” naar de uitgang moet, Rubik’s Cube, en zo voorts. “Nondeju, gij hoort HOERA” 15 In een streven naar een elegante formulering splits ik het probleem op in (1) het genereren van alle “kortste” paden en (2) het testen of een pad eindigt in een doelknoop. Lazy evaluation zal deze afzonderlijk geformuleerde berekeningen in de tijd verweven laten plaats vinden. Een “kortste” pad is: een pad dat in de graaf een kortste pad is van zijn startknoop naar zijn eindknoop. Voor taak (2) ligt de functie voor de hand: kortstePad =head.dropWhile padeinde-is-geen-doelknoop Voor de eenvoud maar even aangenomen dat er altijd een kortste pad bestaat. Voor taak (1) voldoet de volgende functie f; die genereert bij lijst-argument [pad-met-alleen-startKnoop]een lijst van kortste paden vanuit startKnoop naar iedere knoop in de graaf. De definitie is verrassend eenvoudig: f[ ] = [ ] f(p:ps) = p:f(ps ++ qs) waarbij qs = [ pverlengd met k′|k′is buur van eindknoop p die niet zit in p:ps ] Johan, zie je dat feen anamorfisme is? Ik krijg weer warme gevoelens. Een operationele verklaring van de werking luidt als volgt. Na de initiële aanroep f[pad-met-alleen-startKnoop]geldt in iedere aanroep van f: het argument is een lijst van kortste paden vanuit startKnoop die ieder met nul of meer knopen uitgebreid gaan worden. De lengtes van deze paden verschillen hooguit één en de langere paden staan achteraan. Steeds wanneer een pad opgeleverd wordt, worden de 1-staps uitbreidingen daarvan achteraan in het argument van de volgende aanroep van fgezet. Het argument van ffungeert als een queue: het voorste pad p gaat eruit en de nieuwe paden qs komen achteraan. Functie fgenereert de paden in een breadth-first manier. Een formeel correctheidsbewijs zal gebaseerd zijn op deze eigenschap P: P(f) = ∀ps.A(ps)⇒B(ps,f ps) waarbij –A(ps)= “ps is een lijst van kortste paden vanuit eenzelfde startknoop en met lengtes die hooguit één verschillen, gesorteeerd naar oplopende padlengte.” –B(ps,rs)= “rs is een maximale lijst van paden die een (nulof meerstaps) ‘kortste uitbreiding’ zijn van een pad in ps; lijst rs is oplopend gesorteerd naar padlengte.” De implicatie A(ps)⇒B(p:ps,f(p:ps)), gedaan over de linkerkant van de definitie, volgt uit de rechterkant van de definitie en de aanname (inductiehypothese) dat P(f)geldt voor de recursieve aanroep, dat wil zeggen: de aanname A(ps ++ qs)⇒ B(ps ++ qs,f(ps ++ qs)). Dus met inductie naar het aantal unfold-stappen in de berekening, is P(f)waar. 16 Maarten Fokkinga Van paden worden alleen maar eindknopen getest en toegevoegd; daarom representeer ik, binnen f, paden met de startknoop in de staart en de eindknoop aan kop: f(p@(k:_) : ps) = reverse p :f(ps ++ [k′:p|k′←buren k,knietIn p:ps]) Toepassing. Om met fde puzzel op te lossen, moeten we ook de puzzel zelf representeren. Een formele representatie ligt voor de hand en zal ik hier schetsen. Een stuk heeft een naam, breedte en hoogte: (nm,b,h). Het bord heeft posities 0..B−1 in de breedte en 0..H−1in de hoogte. Een configuratie geeft bij ieder stuk een positie: type Configuratie = [(Stuk,Positie)]. Twee geplaatste stukken ((_,b,h),(x,y)) en ((_,b′,h′),(x′,y′)) zijn disjunct als x+b≤x′∨x′+b′≤x∨y+h≤y′∨y′+h′≤y. Een geplaatst stuk ((nm,b,h),(x,y)) zit binnenboord als 0≤x≤B−b∧0≤y≤H−h. Mogelijke zetten vanuit een configuratie czijn als volgt te formaliseren (in zetten :: Configuratie →[Configuratie]). Genereer nieuwe configuraties door íeder stuk van céén positie in één van de vier richtingen te verschuiven (dus 10×4mogelijkheden), op voorwaarde dat het stuk nog binnenboord is en disjunct is van de andere stukken van c. Om de puzzel als graaf te zien kiezen we: Knoop =Configuratie, buren =zetten,startKnoop =beginConfiguratie,doelKnoop =doelConfiguratie. Nondeju. Het duurt te lang voordat het programma een oplossing presenteert voor de jt_Jeuring schuifpuzzel. 4 Hoera Gelukkig zijn er twee aanzienlijke optimalisaties mogelijk: één in de codering van functie fen één in de analyse van de puzzel en puzzels in het algemeen. In de codering van fkan voor de test “nietIn p:ps” een aparte parameter bezocht aan ftoegevoegd worden, en wel een verzameling (uit module Data.Set) van alle geproduceerde knopen. De test wordt dan vervangen door ‘kniet in bezocht’, en in de recursieve aanroep moet het extra argument een geschikte uitbreiding van bezocht zijn. Deze aanpassing reduceert de rekentijd aanzienlijk, met name door de efficiëntere datastructuur. Terzijde. In feite zijn van p:ps hooguit de eindknopen en voorlaatste knopen van de paden nodig. Mijn experimenten suggereren dat deze optimalisatie nauwelijks de rekentijd reduceert maar de code wel compliceert. Diverse andere optimalisaties zijn nog denkbaar, met name de “promotion” van padeinde-is-geen-doelknoop uit kortstePad naar voren in de berekening, tot in fzelf. Ik heb geen optimalisatie gevonden die –voor de puzzel– de rekentijd echt reduceert. Ten aanzien van puzzels in het algemeen realiseer ik me dat verschillende configuraties cen c′equivalent kunnen zijn in de zin dat een zettenreeks naar c en een naar c′allebei evenveel vervolgzetten nodig hebben om tot een gewenste kortste zettenreeks uitgebreid te worden. Voor de schuifpuzzel geldt dat twee “Nondeju, gij hoort HOERA” 17 configuraties equivalent zijn als ze op gelijke posities stukken van gelijke breedte en hoogte hebben; de vier vertikale stukken hebben gelijke breedte en hoogte en dat geldt ook voor de vier kleine vierkante stukken. Ook zijn twee configuraties equivalent als ze gespiegeld zijn langs de vertikale as door het midden. De test ‘kniet in bezocht’ wordt dus vervangen door ‘kis niet equivalent met een knoop in bezocht’. We kunnen dure equivalentietesten vervangen door goedkopere gelijkheistesten, door niet de configuraties zelf op te slaan in bezocht maar ‘unieke representanten van de equivalentieklassen’. Zo’n representant noem ik in puzzeltermen: abstracte configuratie, en in graaftermen: abstracte knoop. Met name, voor de jt_Jeuring schuifpuzzel, geeft een abstracte configuratie bij iedere positie de breedte en hoogte aan, opgeslagen in een lijst gesorteerd naar positie. Twee configuraties zijn equivalent als hun abstracte configuraties gelijk zijn. Met deze twee optimalisaties werkt het programma bevredigend. Voor de schuifpuzzel levert het de oplossing van 112 zetten die aan het begin staat; daarbij worden 23798 zettenreeksen berekend, 77378 configuraties en 23905 abstracte configuraties. Op mijn stokoude PC duurt dat minder dan 8 seconden. Terzijde. Een reeks van 112 configuraties leest wat lastig. Daarom heb ik fiets uitgebreid door niet paden van knopen op te leveren maar paden van transities; een transitie bevat naast de ‘nieuwe’ knoop ook een indicatie van de stap die gedaan is. Functie buren :: Knoop →[Knoop]wordt dus vervangen door transities :: Knoop → [(Stap,Knoop)]. De puzzelaar moet de functie zetten overeenkomstig aanpassen. In de uitkomst van fkan desgewenst de knoop-component verwijderd worden zodat alleen de stappen overblijven. Deze aanpassing heeft geen merkbare invloed op de rekentijd. 5 Een laatste Hoera Tot slot nog een puzzel, speciaal voor jou, Johan. Hoera, hoef jij je het komend weekend niet te vervelen. Vind een kortste reeks plaatswisselingen van letters waarmee start getransformeerd wordt tot eind, waarbij: start = (map toLower.filter isLetter)“Johan Theodoor Jeuring” eind = (map toLower.filter isLetter)“Nondeju, gij hoort Hoera” Vanuit iedere configuratie (letterreeks) zijn 190 verschillende zetten (letterwisselingen) mogelijk, namelijk [(i,j)|i←[0..19],j←[i+1..19]]. Als je dit met de hand oplost, win je het misschien wel van het programma, want op papier zie je zo wat zinvolle wisselingen zijn. Het programma levert de volgende reeks op, met lengte 14: 0-5 0-14 0-4 2-10 2-12 2-18 3-19 3-7 3-17 3-8 3-16 3-13 3-9 6-15 (Hieruit volgt dat 0-5-14-4 en 2-10-12-18 en 3-19-7-17-8-16-13-9 en 6-15 de cycles zijn van een permutatie van start naar eind.) Tijdens de berekening zijn er 361942 reeksen gevormd en 5966258 anagrammen (waarvan sommige al eerder “bezocht” 18 Maarten Fokkinga waren), en bevat bezocht uiteindelijk 365108 anagrammen. De rekentijd was circa 15 minuten; al mijn pogingen om de meest voor de hand liggende lijst-representatie van letterreeksen (en de wisseling van letters!) efficiënter te maken gaven geen reductie van de rekentijd. Johan, ik wens je nog een paar vruchtbare jaren toe in je loopbaan en thuis! Maarten Agda-ventures with PolyP 25 equal0{MaybeNatBoolCode } (inj1tt) (inj2(3, false)) normalizes to false. Note that the first argument to equal0is written in curly braces, marking it as implicit, since it can be inferred. In particular, it is omitted for the recursive calls, and not needed for the example either: we can write just equal0 (inj1tt) (inj2(3, false)). 4 The full story So much for codes for types, and their interpretation as actual types. If we want to handle inductive datatypes as fixpoints, we also want codes for functors. And for polymorphic inductive datatypes, we want bifunctors. So here are three mutually recursive datatypes of codes for them: mutual data Type :Set where NatTy BoolTy UnitTy :Type data Functor :Set where Fix :Bifunctor →Functor data Bifunctor :Set where _∗_ _+_ :Bifunctor →Bifunctor →Bifunctor Const :Type →Bifunctor _•_:Functor →Bifunctor →Bifunctor Par Rec :Bifunctor In order to interpret codes for inductive datatypes, we need to define these: {-# NO_POSITIVITY_CHECK #-} data Mu (f:Set →Set) : Set where In :f(Mu f)→Mu f out : { f:Set →Set }→Mu f→f(Mu f) out (In xs) = xs Not all functors induce inductive datatypes, so we have to turn off the check that Agda would otherwise insist on. Since we are modelling PolyP generating Haskell, we don’t worry too much about the risk of non-termination. We can now give the interpretations of the three kinds of code: mutual [[_]]T:Type →Set [[_]]F:Functor →Set →Set [[_]]B:Bifunctor →Set →Set →Set [[ NatTy ]]T=Nat [[ BoolTy ]]T=Bool 26 Jeremy Gibbons and Patrik Jansson [[ UnitTy ]]T=⊤ [[ Fix f]]Fp=Mu ([[ f]]Bp) [[ f∗g]]Bp r =[[ f]]Bp r ×[[ g]]Bp r [[ f+g]]Bp r =Sum ([[ f]]Bp r) ([[ g]]Bp r) [[ Const t]]Bp r =[[ t]]T [[ d•f]]Bp r =[[ d]]F([[ f]]Bp r) [[ Par ]]Bp r =p [[ Rec ]]Bp r =r Each base code is interpreted as the corresponding base type. Our only code for a functor is for a polymorphic inductive datatype, which is interpreted accordingly, using the interpretation of its bifunctor parameter. Bifunctor codes for lifted product and sum of two bifunctors are interpreted using the standard constructors; the codes for a constant bifunctor and for the composition of a functor and a bifunctor (“@” in PolyP, which is reserved in Agda so written with a bullet here) are defined recursively; and the ‘parameter’ and ‘recursive argument’ are projections. Next we can define the functorial action for functors and bifunctors (the pmap and fmap we saw above), mutually recursive with catamorphisms: mutual {-# TERMINATING #-} pmap : (d:Functor)→(a→b)→[[ d]]Fa→[[ d]]Fb fmap : (f:Bifunctor)→(a→b)→(c→d)→[[ f]]Ba c →[[ f]]Bb d cata : (f:Bifunctor)→([[ f]]Ba b →b)→[[ Fix f]]Fa→b cata f h (In xs) = h(fmap fid (cata f h)xs) pmap (Fix f)g=cata f(In ◦fmap f g id) fmap (f∗g)p r (x,y) = (fmap f p r x ,fmap g p r y) fmap (f+g)p r (inj1x)=inj1(fmap f p r x) fmap (f+g)p r (inj2y) = inj2(fmap g p r y) fmap (Const t)p r x =x fmap (d•g)p r xs =pmap d(fmap g p r)xs fmap Par p r =p fmap Rec p r =r For example, the code ListF for the shape bifunctor for lists, the corresponding code ListC for its fixpoint, and the interpretation MyList of the latter as an actual functor are: ListF :Bifunctor ListF =Const UnitTy + (Par ∗Rec) ListC :Functor ListC =Fix ListF Agda-ventures with PolyP 27 MyList :Set →Set MyList =[[ ListC ]]F We can define constructors for these lists: nilList :MyList a nilList =In (inj1tt) consList :a→MyList a→MyList a consList x xs =In (inj2( ( x,xs ))) and conversion functions from and to built-in lists: toMyList :List a→MyList a toMyList =foldr consList nilList fromMyList :MyList a→List a fromMyList =cata ListF alg where alg :[[ ListF ]]Ba(List a)→List a alg (inj1tt) = [ ] alg (inj2(x,xs )) = x:: xs One canonical example of a polytypic function on polymorphic container datatypes is to “crush” it [11], aggregating the elements using a monoid: mutual crush : (a→a→a)→a→(d:Functor)→[[ d]]Fa→a crush _⊕_ e (Fix f) = cata f(crushB_⊕_ e f ) crushB: (a→a→a)→a→(f:Bifunctor)→[[ f]]Ba a →a crushB_⊕_ e (f∗g) (x,y) = crushB_⊕_ e f x ⊕crushB_⊕_ e g y crushB_⊕_ e (f+g) (inj1x) = crushB_⊕_ e f x crushB_⊕_ e (f+g) (inj2y) = crushB_⊕_ e g y crushB_⊕_ e (Const t)x=e crushB_⊕_ e Par p=p crushB_⊕_ e Rec r=r crushB_⊕_ e (d•g) = crush _⊕_ e d ◦pmap d(crushB_⊕_ e g) The binary operator is used to combine the two aggregations in a product, and the unit value is used for constants. For instance, we can flatten a container to a list, by making every element a singleton list then crushing using the list monoid: flatten : (d:Functor)→[[ d]]Fa→List a flatten d=crush _++_ [ ] d◦pmap d(λx→[x]) 5 Polytypic packing and unpacking Let us now look at a more extended example: another canonical piece of the polytypism literature, namely polytypic packing. By this we mean encoding a value 28 Jeremy Gibbons and Patrik Jansson of arbitrary type as a bitstream, in such a way as to be able (given information also about the type) to decode the bitstream back to the original data. One can think of this as simple-minded data compression. For simplicity, we will encode to lists of bits and ignore the possible refinement of packing the bits into words. We name the bits used to label left and right choices, and provide a case analysis for them: leftBit rightBit :Bool leftBit =false rightBit =true caseBit :Bool →a→a→a caseBit b x y =if bthen yelse x the idea being that b=caseBit bleftBit rightBit We provide primitives toBits and fromBits to convert between natural numbers and lists of booleans (making the simplifying assumption that all numbers are distinct to bitWidth bits—we could be cleverer about this): bitWidth :Nat bitWidth =4– we keep it small for testing toBits :Nat →List Bool toBits n=reverse (go bitWidth n)where go :Nat →Nat →List Bool go zero n=[ ] go (suc m)n=let (q,r)=divMod2 nin r:: go m q fromBits :List Bool →Nat fromBits =foldl (λn b →(2∗Nn)+N(if bthen 1else 0)) 0 Now, as a first attempt we might represent a packer for data as a function from that data to lists of bits. However, an unpacker would have to be more than simply a function in the opposite direction: we have to return the unused bits too, in order to be compositional; and we have to allow for failure, to make a total function. So we define the following: Unpacker :Set →Set Unpacker a=List Bool →Maybe (a×List Bool) In fact, that type supports a monad—the combination of the state monad transformer on bit-list state around the maybe monad, what would in Haskell be written StateT [Bool]Maybe: P:Set →Set P=Unpacker Agda-ventures with PolyP 29 It turns out to be convenient to define packer using the same type: Packer :Set →Set Packer a=a→P⊤ A packer will always succeed, and will produce rather than consume some bits. In that sense, the Pmonad is overkill—but it allows u now to think about composing packers and unpackers. Note that an unpacker Unpacker Afor some type Ais isomorphic to a function of type ⊤→PA, which is nicely dual to the packer type A→P⊤. (For more on this duality, see [6].) The stateful interface is provided by two operations: put :Packer (List Bool) put bs’ =λbs →just (tt , bs’) get :Unpacker (List Bool) get =λbs →just (bs ,bs) But we will not need the full power of these two operations; we will use them only in restricted ways. For packers, we need only add some output: packerTell :Packer (List Bool) packerTell bs =do bs’ ←get put (bs ++ bs’) (for reasons that will become clear in due course, we prepend rather than append). In particular, here are primitive packers for naturals, booleans, and the unit type: packNat :Packer Nat packNat n=packerTell (toBits n) packBool :Packer Bool packBool b=packerTell [ b] packUnit :Packer ⊤ packUnit tt =return tt Note that packUnit is a no-op. Primitive unpackers for naturals and units are similarly easy: unpackBool :Unpacker Bool unpackBool =uncons unpackUnit :Unpacker ⊤ unpackUnit =return tt To unpack a natural, we read a chunk of input, then convert these bits to a number: unpackNat :Unpacker Nat unpackNat =do 30 Jeremy Gibbons and Patrik Jansson xs ←get let (ys ,zs)=splitAt bitWidth xs put zs return (fromBits ys) 5.1 Packing as a monadic catamorphism Now, to pack a structure of an inductive datatype, we will use a monadic catamorphism [12], which is like the ordinary catamorphism except that the algebra argument and the catamorphism itself are Kleisli arrows—that is, they have a monadic return type: mutual cataM : (f:Bifunctor)→([[ f]]Ba b →Pb)→[[ Fix f]]Fa→Pb We will return to the definition of cataM shortly; but let’s first see how it is used. We define three mutually recursive functions, packers respectively for a type, a functor, and a bifunctor, taking correspondingly many element packers as arguments: packT : (t:Type)→Packer [[ t]]T packF : (d:Functor)→Packer a→Packer ([[ d]]Fa) packB : (f:Bifunctor)→Packer a→Packer b→Packer ([[ f]]Ba b) The packers for types each delegate to the appropriate primitive defined earlier: packT NatTy n=packNat n packT BoolTy b=packBool b packT UnitTy tt =packUnit tt We only have one code for functors, interpreted as an inductive datatype, and this is where we use the monadic catamorphism: packF (Fix f)p=cataM f(packB f p packUnit) The catamorphism handles the recursive calls, so at the top level we do nothing (packUnit) for the recursive positions. Finally, we have one fairly simple case per bifunctor: packB (f∗g)p q (x,y)=do packB g p q y packB f p q x packB (f+g)p q (inj1x) = do packB f p q x packerTell [ leftBit ] packB (f+g)p q (inj2y) = do packB g p q y packerTell [ rightBit ] packB (Const t)p q =packT t Agda-ventures with PolyP 31 packB (d•g)p q =packF did ◦pmap d(packB g p q) packB Par p q =p packB Rec p q =q Recall that the primitive operations to write bits were defined to prepend to the list. We therefore specify that for products, we pack the right then the left component of the pair; then the left component will appear first in the output. Similarly— and more importantly—for sums, we emit the discriminator bit after packing the payload. Now back to the monadic catamorphism. This requires a distributive law of the shape bifunctor over the monad—informally, this hoists the monad to the top, executing the computations for each of the recursive positions to make one composite computation collecting all the effects: distr : (f:Bifunctor)→[[ f]]Ba(Pb)→P([[ f]]Ba b) Then the catamorphism deconstructs the data, makes recursive calls on each of the children, collects all their effects, applies the algebra h, and merges the effects of that: {-# TERMINATING #-} cataM f h (In xs)=join (h<$> (distr f(fmap fid (cataM f h)xs))) Note that the catamorphism is bottom up: the effects from children are incurred before those of the parent. This is why we defined the primitive packers to prepend bits instead of appending them: the encoding of the root of the data structure will end up at the start of the output list, conveniently for unpacking. The last ingredient is the distributive law. This is in essence another polytypic program, with mutually recursive definitions for functors and bifunctors (types are not needed): distrF : (f:Functor)→[[ f]]F(Pa)→P([[ f]]Fa) distrB : (f:Bifunctor)→[[ f]]B(Pa) (Pb)→P([[ f]]Ba b) distrF (Fix f) (In xs) = In <$> (distrB f(fmap fid (distrF (Fix f) ) xs)) distrB (f∗g) (xs ,ys)=liftM2 _,_ (distrB f xs) (distrB g ys) distrB (f+g) (inj1x) = inj1<$> distrB f x distrB (f+g) (inj2y) = inj2<$> distrB g y distrB (Const t)x=return x distrB (d•g)xs =distrF d(pmap d(distrB g)xs) distrB Par x=x distrB Rec x=x The variant we actually use is for bifunctors, but with pure values in the parameter positions, so we must first inject these into the monad: distr f=distrB f◦fmap freturn id 32 Jeremy Gibbons and Patrik Jansson For example, with bit width set to 4 for brevity, the expression packF ListC (packT NatTy) (toMyList (1:: 2:: 3:: [ ])) [ ] reduces to the expression in Figure 1. just (tt , true :: false :: false :: false :: true :: – toBits 1 true :: false :: false :: true :: false :: – toBits 2 true :: false :: false :: true :: true :: – toBits 3 false :: [ ]) Fig. 1. The list of bits resulting from packing 1, 2, 3 is true to indicate a cons cell, then four bits representing the number 1, then similarly for the next two elements, then false to indicate a nil cell. 5.2 Unpacking as a monadic anamorphism Let us now turn to unpacking. Being the inverse of packing, it will use the dual pattern: a monadic anamorphism, which is again like the ordinary anamorphism only where the coalgebra and the anamorphism itself are Kleisli arrows: mutual {-# TERMINATING #-} anaM : (f:Bifunctor)→(b→P([[ f]]Ba b)) →b→P([[ Fix f]]Fa) Unpacking is again defined in terms of three mutually recursive functions, unpackers respectively for types, functors, and bifunctors, each with the corresponding number of element unpackers as arguments: unpackT : (t:Type)→Unpacker [[ t]]T unpackF : (d:Functor)→ Unpacker a→Unpacker ([[ d]]Fa) unpackB : (f:Bifunctor)→ Unpacker a→Unpacker b→Unpacker ([[ f]]Ba b) For the base types we defer to the earlier primitives: unpackT NatTy =unpackNat unpackT BoolTy =unpackBool unpackT UnitTy =unpackUnit Agda-ventures with PolyP 33 For the sole functor code, we use the anamorphism: unpackF (Fix f)u=anaM f(λ_→unpackB f u unpackUnit) _ Note that the ‘seed’ of the anamorphism is the unit type: all the information driving the computation comes from the list of booleans, encoded in the monad. So the bound variable of the lambda is irrelevant, and the initial seed of the anamorphism can be inferred. As with packing, the anamorphism handles the recursive calls, so at the top level we need do nothing for the recursive positions (unpackUnit, another no-op). And finally, there is one fairly simple case per bifunctor: unpackB (f∗g)u v =liftM2 _,_ (unpackB f u v) (unpackB g u v) unpackB (f+g)u v =do b←unpackBool caseBit b (inj1<$> unpackB f u v) (inj2<$> unpackB g u v) unpackB (Const x)u v =unpackT x unpackB (d•g)u v =unpackF d(unpackB g u v) unpackB Par u v =u unpackB Rec u v =v For products, we unpack the left then the right components; for sums, we consume one discriminator bit in order to decide which branch to take. Now back to the monadic anamorphism. This applies the coalgebra to the seed, makes recursive calls to generate each of the children, collects all their effects, merges the effects from the coalgebra and the recursive calls, then wraps the result up in the constructor: anaM f h y =In <$> join (distr f<$> (fmap fid (anaM f h)<$> h y)) To illustrate the round trip, it should be the case that whatever value we take, if we pack it in front of any bit sequence then unpack the resulting sequence, that composition should succeed, and should return the original value and sequence: packUnpack : { a:Set }→Packer a→Unpacker a→a→List Bool →Set packUnpack p u x bs = (p x »u)bs ≡just (x,bs) (recall that a packer returns unit, which we then discard by »). Then we can instantiate this scheme for the types, functors, and bifunctors in our universe: packUnpackT : (a:Type)→[[a]]T→List Bool →Set packUnpackT a=packUnpack (packT a) (unpackT a) packUnpackF : (d:Functor)→(a:Type)→[[d]]F[[a]]T→List Bool →Set packUnpackF d a =packUnpack (packF d(packT a) ) (unpackF d(unpackT a) ) 34 Jeremy Gibbons and Patrik Jansson packUnpackB : (f:Bifunctor)→(a b :Type)→ [[f]]B[[a]]T[[b]]T→List Bool →Set packUnpackB f a b =packUnpack (packB f(packT a) (packT b) ) (unpackB f(unpackT a) (unpackT b) ) For example, we can check the round trip property on a list of three naturals: packUnpackList :∀(bs :List Bool)→ packUnpackF ListC NatTy (toMyList (1:: 2:: 3:: [ ])) bs packUnpackList bs =refl The value we give to packUnpackList is simply refl, which indicates that (and is only type correct when) the two sides of the equivalence are definitionally equal. 6 Discussion The technique we have used of identifying an algebraic datatype of codes for types drawn from some universe is a standard pattern in dependently typed programming. It is an instance in microcosm of the “formulation á la Tarski” that MartinLöf [10] used in macrocosm to construct a universe of discourse for intuitionistic type theory. Another way of looking at it is specifying an embedded domain specific language for types (namely the codes), and semantics by way of a shallow embedding into the host language (namely the interpretation) [2]. This paper is literate Agda, although some of the gory details have been elided for presentation purposes. The full story can be seen in the source, which is available on GitHub [4], and typechecks at least with version 2.7.0.1 of Agda and version 2.2 of the Agda standard library. We have seen that the polytypic programming features that Johan pioneered with PolyP can be done nowadays as ‘mere programming’, given a sufficiently rich language—in particular, a dependently typed one. We have chosen Agda, but Idris would work just as well. Even Haskell is almost powerful enough these days: much of the PolyP functionality was achieved in Haskell already in 2003 [14]. But dependent types have the additional advantage that proofs become part of the language. We have exploited this briefly above: the code contains some unit tests, which are run as part of typechecking. And indeed we have exploited these tests while writing the programs: although many silly errors are ruled out by the types, it is in particular still possible to write out the wrong bit sequences. But a powerful and informative type system like Agda’s is not just there to prevent accidents. It is also hugely valuable when it comes to writing the programs in the first place: the type specifies much about the program, so with suitable interaction between the type checker and the editor—for example, in the Agda mode for Emacs—much of the program can be written automatically. Some values can be inferred; case analyses can be automatically generated; programs can be Incremental Optimal-Fit Line Breaking 41 The length (number of elements) of list xis given by #x.The empty list will be written as [ ],the singleton list containing a single element awill be written as [a], that of two elements aand bas [a,b],and so on. The concatenation of two lists xand yis denoted by x++y.Prepending an element ato a list xwill be denoted by the operator ≻ ⊢,also known as cons, while appending it will be denoted by the operator ⊣ ≺,also known as snoc. They can be defined more formally by: a≻ ⊢x= [a]++ x; x⊣ ≺a=x++[a]. The function ([ ]⊣ ≺) : A→A+forms a singleton list. We could equally have written (≻ ⊢[ ]),but will use the symmetric notation [·], so [·](a)=[a]. Map. Given function f:A→B,its extension to the map function f∗:A∗→B∗is characterized by: f∗[ ] = [ ]; f∗[a] = [f(a)]; f∗(x++y) = f∗(x)++f∗(y). For example, if succ is the function assigning to each letter in the Latin alphabet its successor (with succ(Z) = Ato complete the circle), we have succ∗[H,A,L] = [succ(H),succ(A),succ(L)] = [I,B,M]. Map distributes over function composition, as expressed by the functional identity (f◦g)∗= (f∗)◦(g∗). Reduce. Let (A,⊙, ν⊙)be a monoid with carrier set Aand a binary associative operation ⊙:A × A → A with neutral element ν⊙.Then ⊙/:A∗→ A is characterized by: ⊙/[ ] = ν⊙; ⊙/[a] = a; ⊙/(x++y) = (⊙/x)⊙(⊙/y). For example, +/[4,6,3] = 4 + 6 + 3 = 13,and ++/[[a],[ ],[b,c]] = [a]++[ ]++[b,c] = [a,b,c]. Filter. Let ⊤and ⊥stand for the truth values true and false, together forming B={⊤,⊥}.Given a predicate p:A→Bdefined on list elements that tests whether they are “worthy” of being kept, we can combine reduce and map to define a function p◁:A∗→A∗that filters out the worthy elements of a list and discards the rest. We first define a (purely auxiliary) function p?:A→A∗defined by: p?(a) = [a] if p(a) = ⊤ [ ] if p(a) = ⊥. 42 Lambert Meertens Our filter function p◁is then defined as: p◁(x) = ++/(p?)∗(x). For example, if odd tests whether a natural number is odd, we have odd◁[3,4,5] = ++/(odd?)∗[3,4,5] = ++/[odd?(3),odd?(4),odd?(5)] = ++/[[3],[ ],[5]] = [3]++[ ]++[5] = [3,5]. Application to sets. Finite sets can be represented by lists; for example, [2,3,1], and [3,1,2,1] are different representations of the set {1,2,3}.If we think of concatenation ++ as implementing set union ∪for sets represented by lists, the definition of f∗given above works equally well for sets represented by lists, regardless of the particular representation. This holds likewise for ++/(implementing S) and p◁. For this to work for ⊙/in general, the operation ⊙needs to be also commutative and idempotent. Since ∧is both, ∧/can be thought of as working on sets of truth values. Inits, tails and segments. Function inits :A∗→A∗∗ returns a list of all initial segments of its argument, so inits [a,b,c] = [[ ],[a],[a,b],[a,b,c]]. It can be defined by inits [ ] = [[ ]]; inits(a≻ ⊢x) = [[ ]] ++ (a≻ ⊢)∗(inits(x)). Its mirror image, function tails :A∗→A∗∗,returns a list of all tail segments of its argument, so tails [a,b,c] = [[a,b,c],[b,c],[c],[ ]]. It can be defined by tails [ ] = [[ ]]; tails(x⊣ ≺a) = (⊣ ≺a)∗(tails(x)) ++ [[ ]]. All segments of a list are then given by: segs = ++/◦tails∗◦inits. So segs [a,b,c] = [[ ],[a],[ ],[a,b],[b],[ ],[a,b,c],[b,c],[c],[ ]].A list of length nhas in total (n+1)(n+2)/2segments, of which n+1 are empty. Partitions. A partition of a list xis a list whose elements are nonempty segments of x,such that, concatenated together, they give us back the original list x.For example, [[7,0],[7],[2,4,5]] is a partition of [7,0,7,2,4,5].Defining auxiliary predicate pop (for “populated”) on lists by pop(x) = (#x>0),function parts :A∗→(A+)∗is such that parts(x)represents the set of partitions {xs |xs =pop◁(xs)∧(++/xs =x)}. Optimum selection w.r.t a criterion. Let f:A→Pbe a function from some domain Ato a totally ordered codomain P,representing a criterion that will guide Incremental Optimal-Fit Line Breaking 43 the selection of an optimal choice. Rather than awarding points for goodness of fit, we measure the cost of a candidate, so a lower score means a better fit. (The letter Pis the first letter of penalty.) For our application we can use the extended set of nonnegative reals {x∈R|0≤x} ∪ {+∞},while using Nor Qinstead of R also works. The value +∞is meant to be given to a choice that is so egregiously bad that it can be discarded prima facie (possibly implemented as a number that is so high, such as 999999,that all other choices have a lower penalty). We define: x↓fy=xif f(x)≤f(y) yif f(y)<f(x). A determinate choice between two equally good candidates — with this definition the first of the two — is pragmatically desirable. 2 Problem statement We now have the ingredients to specify the problem more formally. The input text is not just a list of characters. Instead, it is a preprocessed list of chunks determined by the points in the raw input text where a linebreak might occur, which can be in the middle of a word if hyphenation is possible. The begin point and end point of the text are also counted as break points, possibly the only break point if the text is empty. These (potential) break points are used to break up the text in chunks, and the list of these chunks forms the input. For example, the raw input an incredibly important development can be chunked (for a system allowing hyphenation) into this list of 12 chunks: [an⊔,in−,cred−,i−,bly⊔,im−,por−,tant⊔,de−,vel−,op−,ment⊔], in which marking a chunk with ⊔signals that in typesetting the chunk should be followed by a blank space unless it is the last chunk on a line, while −signals that the chunk should be followed by a hyphen if at the end of a line, and otherwise be joined without intervening space to the next chunk. The treatment in this article will not consider how these chunk lists are represented, but one possibility for a practical implementation is that of a doubly-linked list, so that edit operations in the middle of the text need no more than O(1) cost. Given the input list x:A+of text chunks, the partitions of the list correspond to the potential ways of breaking up the text into lines. We assume that a function slpen :A→Pis given for assigning a penalty to a single line of a partition. The 44 Lambert Meertens total penalty pen = +/◦slpen∗,obtained by summing the individual penalties of the lines of a partition, can be used to determine an optimal-fit line breaking of a given paragraph; in a formula, ↓pen/parts(x). Function pen is monotonic with respect to concatenation: pen(x)≤pen(y)⇒pen(u++x++v)≤pen(u++y++v) for all lists x,y,uand v.An equivalent formulation of this monotonicity property is the statement that concatenation ++ distributes over optimal choice ↓pen : u++(x↓pen y)++v= (u++x++v)↓pen (u++y++v). If there is no way a chunk segment scan fit on a single line, partitions having s as an element should be avoided. This is modeled by then taking slpen(s) = +∞. Other than that, the single-line penalty function can be almost arbitrary; we shall introduce a pragmatic assumption below. Generality of the penalty function is important for quality typesetting. A simple penalty function for a single line found in the literature is the combined width of blank space, sometimes referred to as waste. However, this is overly simplistic, particularly for justified typesetting, in which both margins are adjusted. Then the combined blank space is divided between the words on the line. The total width of blank space, divided evenly into the three spaces between four words, may look just fine. When the same amount of space separates just two words, the result may be jarring. Also, sometimes a better overall fit can be achieved by squeezing the words on a line just a tiny bit together. This should come at a cost; the squeezing should incur a penalty, even if the “waste” is reduced. Another issue is that not all break points are created equal. All else being the same, breaking between two words is better than resorting to hyphenation to break inside a word, and breaking after a full sentence or a comma is better than breaking just anywhere between two words. In the famous sentence ALL YOUR BASE ARE BELONG TO US, breaking the line as in ALL YOUR BASE /ARE BELONG TO US is easier on the reader than ALL YOUR BASE ARE /BELONG TO US. A limitation of the specification is that all lines are treated the same, so it does not accommodate a varying distance between the margins, as when text flows around a figure. Pagination also falls outside the scope of the problem as considered here. The last line of a paragraph should also get a special treatment; the line is not adjusted, and an ample amount of blank space should not be penalized. Fortunately, Incremental Optimal-Fit Line Breaking 45 this can easily be accommodated. The invoker slpen∗of the application of slpen to each of the chunk segments of a partition “knows” when this function is applied to the last segment and can then substitute a last-line variant. Pragmatic assumption. Since lines are not infinitely wide, and chunks are not infinitely thin, there is an upper bound on the number of chunks that can fit on any line. We assume that a reasonably low value βof such an upper bound is known, and that chunk segments that are too large to fit on a line get the maximal penalty, so that #s> β ⇒slpen(s) = +∞. 3 Theory Dags. A dag (directed acyclic graph) (N,E)consists of •a set of nodes Nand •a set of edges E ⊆ N × N , •such that the transitive closure E+is irreflexive — there is no path from a node to itself. The meaning of (s,t)∈ E is that there is an edge from node sto node t. Partial orders. A partial order (A,⊑)consists of •a set Aand •a relation ⊑ ⊆ A ×A, •such that ⊑is transitive, reflexive and antisymmetric. Po-dags and weighted dags. A partial order (A,⊑)can be turned into a dag as follows. Take the irreflexive relation (<)=(⊑)\IA,where IA={(a,a)|a∈ A} ⊆ A ×A.Then (A,<)is a dag, which we refer to as the po-dag of the partial order. The partial order can be recovered from its po-dag by using (⊑)=(<)∪IA. Given a list xof length #x=n,there is a bijection between the elements of parts(x)and the paths in the po-dag of ({0, ..., n},≤).Each edge (s,t)in a path corresponds to a segment of length t−sof the partition. This bijection plays an important role in what follows. If the edges have “lengths”, and the length of an edge is the penalty of the corresponding spanned segment, a shortest path from 0to nin the po-dag corresponds to an optimal-fit line breaking of paragraph x. Such valuations of edges are more commonly called weights. AV-weighted dag (N,E,V,w)comprises: •a dag (N,E), •a set of weights V,and •a weight function w:E → V. 46 Lambert Meertens In our application, V=P.We will use matrices, treated later, to represent weighted dags. Dioids. A dioid (a.k.a. semiring)(A,⊕, ν⊕,⊗, ν⊗)comprises: •a commutative monoid (A,⊕, ν⊕)and •a monoid (A,⊗, ν⊗)over the same carrier, •such that ⊗distributes over ⊕. The distributivity property implies (and is implied by) the functional identities (a⊗)◦⊕/=⊕/◦(a⊗)∗; (⊗a)◦⊕/=⊕/◦(⊗a)∗. It also implies that ν⊕is a zero of operation ⊗. Dioids include: •rings, e.g. (Z,+,0,×,1), •complete semilattices, e.g. (P,↓id,+∞,+,0),also called a “tropical semiring”, •regular algebras, introduced later on. Sparse and full matrices. Let Nnstand for the set {0, ..., n}(of size n+1). A (sparse) V-matrix (E,V,M)consists of •a set of index pairs E ⊆ Nn×Nnfor some n∈N, •a set of values V, •a function M:E → V. Instead of M(i,j)we use the conventional notation Mi,j,with the index pair as a subscript. A function f:V → W can be extended to a map function f∗from V-matrices to W-matrices with the same set of index pairs by defining (f∗(M))i,j=f(Mi,j), which amounts to replacing M:E → V by f◦M:E → W. When E=Nn×Nn,we have a full square matrix. By adjoining a new element ⊥ (representing a “missing entry”) to V,defining V⊥=V ∪ {⊥},we can conceptually extend a sparse V-matrix (E,V,M)with E ⊂ Nn×Nnto a full V⊥-matrix (Nn× Nn,V⊥,M⊥,)where (M⊥)i,j=Mi,jif (i,j)∈ E ⊥if (i,j)∈ E . The sparse matrix can be reconstructed from the full version by taking E= {(i,j)|(M⊥)i,j=⊥}.In what follows, we shall switch tacitly between the sparse and the full view. Incremental Optimal-Fit Line Breaking 47 As is somewhat obvious from their formal definitions, V-weighted dags whose nodes are natural numbers are also V-matrices. The converse is not necessarily true; a V-matrix viewed as a graph is not necessarily acyclic. But one is a subspecies of the same species of animal in the mathematical zoo, so rather than one being “represented” by the other, they actually represent different modes of contemplating the same object. Ultimately, the partitions of a chunked input text, together with a penalty function, can be viewed as a P-weighted dag and therefore as a P-matrix. A matrix thus obtained is an upper triangular matrix. Nested-list view. We can encode a full matrix (Nn×Nn,V⊥,M⊥)as a vector of column vectors. Since these vectors have finite lengths, they can be represented as lists. The full matrix view can be recovered from the nested-list view in an obvious way. We shall also switch tacitly between the structure view and the nested-list view on matrices. For example, if the full version of Mis an n×nmatrix, and vis a vector of length n+1,the full version of M⊣ ≺vis an (n+1) ×(n+1) matrix. Snoccing, successively, vectors of length 1, 2, ... onto an initially empty matrix results in an upper triangular matrix. Matrix dioids. A dioid (A,⊕, ν⊕,⊗, ν⊗)induces a dioid on A-matrices sharing their (full) index-pair set Nn×Nn, whose “funny plus” and “funny times” are defined by (M⊕N)i,j=Mi,j⊕Ni,j; (M⊗N)i,j=⊕k(Mi,k⊗Nk,j). As with conventional matrices from linear algebra, these operations preserve uppertriangularity. Regular algebras. A regular algebra (A,⊑,◦,I)comprises: •a complete lattice (A,⊑),for which we denote the join by ⊔and bottom by ⊥,and •a monoid (A,◦,I), •such that (x◦)and (◦x)are universally ⊔-junctive for all x∈ A — that is, they are monotonic and continuous. Given a regular algebra (A,⊑,◦,I),we have that (A,⊔,⊥,◦,I)is a dioid. If we apply the matrix dioid construction to a dioid derived from a regular algebra, the resulting matrix dioid also corresponds to a regular algebra, but now a regular algebra of matrices. Examples of regular algebras: •(P,≤,+,0). 48 Lambert Meertens •For any monoid (A,⊕, ν⊕)we have that (P(A),⊂,X⊕,{ν⊕})is a regular algebra, in which P(A)stands for the powerset of A,and the operator X⊕ is defined by xX⊕y={a⊕b|a∈x∧b∈y}. For the latter construction, it is worth remarking that the monoid (A∗,++,[ ]) gives rise to the well-known language algebra, the regular algebra of languages over an alphabet A. In a regular algebra we can define the Kleene plus operation __+:A → A,informally described by x+=x⊔x◦x⊔x◦x◦x⊔... . A precise characterization is given by c=x+⇔c◦c=c∧ ∀(y:y◦y⊑y:x⊑y⇔c⊑y). For the matrix regular algebra, the Kleene plus is M+=M⊕M2⊕M3⊕... , in which M1=Mand Mn+1 =Mn⊗M. If Mis a triangular matrix with indexpair set Nn×Nn,all powers Mk,for k>n,are the same; they are all equal to the neutral element of the matrix operation ⊕, the matrix all of whose entries are the neutral ν⊕of the carrier. It follows that the computation can be performed in a finite number of steps. If Mis triangular, then, by the preservation of triangularity by the operations ⊕ and ⊗, so is M+.It follows that M+can be computed incrementally, column-wise, by the repeated application of the identity (M⊣ ≺v)+=M+⊣ ≺(M+⊗v). Dioid morphisms and regular-algebra morphisms. Both types of morphisms are defined in the obvious way. So a dioid morphism hsatisfies h(x⊕y) = h(x)⊕′ h(y),and so on, where the prime indicates this is the operation of the target dioid. Note that a regular-algebra morphism satisfies, in particular, h◦F=F′◦h∗. If (A,⊕, ν⊕,⊗, ν⊗)is a dioid, the function ⊕/:P(A)→Ais a dioid morphism, from dioid (P(A),∪,{},X⊗,{ν⊗})to dioid (A,⊕, ν⊕,⊗, ν⊗). If the target dioid is a regular algebra, this is also a regular-algebra morphism. Finally, if his a regular-algebra morphism, then so is h∗on the corresponding matrix algebra. 4 Development The time has come to apply all this machinery to the problem. We begin by creating, seemingly, more work. The function Incremental Optimal-Fit Line Breaking 49 Segs :A∗→A∗∗∗ =tails∗◦inits turns a given list into a matrix of all segments of the given list (using the nestedlist view of a matrix). We have seen this function before, anonymously, in the definition of function segs (with a lower-case s). Using lower-case segs, upper-case Segs could have been defined by: segs = ++/◦Segs :A∗→A∗∗. The partitions function mapped over a segment matrix gives rise to an important identity: parts∗(Segs(x)) = ({[·]}∗(Segs(x)))+, in which {[·]}maps ato {[a]}and the Kleene plus is that of the regular matrix algebra derived from the language algebra. This is a formal expression of the correspondence, mentioned earlier, between partitions and paths. We map the optimal selection over the segment matrix and calculate: (↓pen /◦parts)∗(Segs(x)) = ↓pen /∗(parts∗(Segs(x))) = ↓pen /∗(({[·]}∗(Segs(x)))+) = ((↓pen /◦{[·]})∗(Segs(x)))+. = ([·]∗(Segs(x)))+. The disappearance of ↓pen from the final expression deserves an explanation. While the Kleene plus in the earlier expressions is that of the regular matrix algebra derived from a (∪,X++)algebra, in the final step the morphism ↓pen /turns it into the Kleene plus of the regular matrix algebra derived from a (↓pen ,++) algebra. So ↓pen has not truly vanished; the operation is hiding in the application of __+. There is no need to compute the full matrix; if #x=n, x=Segs(x)0,n, parts(x) = (parts∗(Segs(x))0,n, and so on. So we are actually only interested in the top row. Letting Mi,∗stand for the ith row [Mi,0,Mi,1,Mi,2, ...]of M, we have, for the top row of interest: ((M⊣ ≺v)+)0,∗=M+ 0,∗⊣ ≺(M+ 0,∗⊗v), 50 Lambert Meertens in which ⊗is the “scalar product” of two vectors. Therefore the function f= (↓pen/◦parts)∗◦inits can be computed in a scan, using f(x⊣ ≺a) = f(x)⊣ ≺(f(x)⊗tails(x⊣ ≺a)). By symmetry, there is an analogous expression for g(a≻ ⊢y)for the mirror-image function g= (↓pen/◦parts)∗◦tails. The stage is now set for the final act, incrementalization. The object on which the computation proceeds is a pair of chunk lists (x,y), being the chunks before and after the edit cursor. The pair (x,y)represents the current (chunked) input text x++y, but with the edit focus represented. (If the cursor actually falls inside a chunk, we can treat this as if the cursor is behind that chunk.) The cursor movements left and right correspond then to (x⊣ ≺a,y) LEFT −→ ←− RIGHT (x,a≻ ⊢y). The edit operations of inserting a chunk aand deleting a chunk correspond to (x,y) INSERT a −→ ←− DELETE (x⊣ ≺a,y). Changes inside a chunk can be treated as the deletion of the chunk followed by the insertion of the changed chunk. Incrementalization is not yet achieved by incrementally maintaining the pair of lists (f(x),g(y)),updating these on each operation. These lists need to be ”glued” together to find f(x++y)n,where n= #(x++y). To this end, we extend f(x)to f(x++z),where zis a sufficiently long initial segment of y,meaning that either pen(z) = ⊥(no need to look further because all the rest will be ⊥’s) or z=y(we cannot go further). The claim that we need not look further after meeting a ⊥is a theorem of regular algebra. Specifically, the assumption b◦a=⊥implies b◦a∗=b.Using this, we also obtain that this assumption implies the equality (a⊔b)+ ={closure} (a⊔b)◦(a⊔b)∗ ={regular algebra} Algorithmics for Unicians 57 lc*|+ The advantage in algorithmics is that we can generalise this to a more widely applicable rule, namely that for applicable functions fand h, h(++/arg) is equivalent to f/(h*arg) The applicability rule is as follows: a ‘homomorphism’ is any function that can be expressed as a combination of a reduction on a map: h arg = f/g* arg This includes all maps and reductions themselves, since f/arg = f/id*arg where id is the identity function, and g*arg = ++/G*arg where G arg = [g arg] In a definition of a homorphism h h = f/g* we say that gis the operation ‘of’ h. The applicability rule for h ++/ = f/h* is that his a homomorphism, and fis its operation. So going back to our example, # ++/ dir = +/#*dir can we show that #is a homomorphism with operation +? The answer is yes: Let one: be the function that no matter what its argument, returns the value 1. Then we can define #as +/one* But now we have our general rule, we can apply it to other expressions, and not just to cat and lc. 58 Steven Pemberton References 1. E. W. Dijkstra, The Discipline of Programming, Prentice-Hall, 1976. ISBN 0-13215871-X. (Preface, p. xvii, last line before the acknowledgements) Postscript: Why I never write articles in LATeX There was a time when I was an absolute expert in the use of Troff. I wrote articles, books, even letters in it. And I hated it. But, alas, there was no alternative. It had an atrocious mental model (if you can even claim it had one), and was akin to using assembly language. So I greatly looked forward to the announced arrival of TeX, which would enable me to dump Troff for good. You may be aware that the original edition of Volume 1 of Knuth’s The Art of Computer Programming, published in 1962, (which I bought and still own) listed the seven volumes of the series, saying that they would ‘soon’ be published (this was obviously some strange use of the word ‘soon’ that I wasn’t previously aware of). Now, as I contemplate the parts of volume 4 as they are published, the third having just been published in February of this year, and consider his age (87 at the time of writing), I think he is not doing us any great favours: I want all those volumes, and I’m not going to get them. (It also puts into perspective how he started thinking about TeX in 1977, and planned to have it finished by 1978, but didn’t finish it until 1989 -- if it can actually be said to have been finished.) But I digress. Let me explain my philosophical position: a document is an abstraction. It consists of a title, an author or more, sections with a heading, and paragraphs that consist of words. There are figures and images, and equations. Different publications have their own rules for how an article should be displayed. That’s their problem, and it should absolutely not be the responsibility of the author how a document is represented. That’s what style sheets are for. Any different representation of a given article is still the same article. It just looks different. This is absolutely not the approach of tEx. It is all about representation, and not about abstraction. Big mistake. So when I first used it I was immensely disappointed. I should point out I haven’t used it in years, because I was so quickly put off, but I remember the thing that finally turned me off was the justification algorithm: if it couldn’t find a decent solution for a line of output, it would allow the text to extend into the margins, and let the author solve the problem. This was for me the worst of all possible outcomes, the ugliest possible result: if I made a change in a document, I had to recheck the whole output to make sure it didn’t have any new unresolved lines. This meant I couldn’t trust it to put it into a publishing pipeline. Apart from its lack of proper abstraction, its preoccupation with representation, and its faulty display routine, there was one other thing that disturbs me. Research had been done in the effect of authoring tools on the quality and quantity of content produced. The result showed that writing by hand produced Algorithmics for Unicians 59 low quantity and high quality, writing using a mark-up system like lAtEx or Troff that you had to compile to get the result, produced high quantity but lower quality, and using WYSIWYG produced high quality and high quantity. It was this result that led me to start writing my diary every day with a WYSIWYG editor, and produce all my articles and papers similarly using WYSIWYG, using an abstract document type (based on XML) with style sheets for representation. This includes articles, letters, and books: style-sheets are these days very powerful. And so all of a sudden my content is reusable: throw in a new style sheet, and the article can be presented as the slides of the talk about the article, and let the style sheet do the work. Pax et Bonum Alberto Pettorossi Università di Roma Tor Vergata Dear Johan, my best wishes for your sixtieth birthday. Thanks for everything you have done with much dedication and enthusiasm throughout so many years in your university and in our community of the IFIP Working Group 2.1. Your scientific contributions have been very valuable and stimulating for all of us and for me, in particular. Your activity has been a source of encouragement and strength. I appreciate the example you have given us and you continue to give,as an illuminating researcher and a dedicated teacher. I wish you all the best so that you may continue for many years ahead, your activity at your university and within our Working Group. With great esteem, “Pax et Bonum” from the old colleague and friend of yours, Alberto Letters that are not just words Marc van Kreveld Recently I learnt that Johan has a special interest in palindromes, to be found in strings. Palindromes are about ordering of letters without being about the meaning of the words. In 2013 Johan wrote a scientific text on finding palindromes on the occasion of the 61st birthday of Rinus Plasmeijer. There are other ways in which one can be interested in letters without the text they might represent, for example as shapes. And with shapes we get to my area of expertise: geometry. Geometry extends the basic linear ordering important to palindromes to a less well-defined ordering in twoor three-dimensional space. So it is only fitting that I spend a few lines of text connecting letters to Johan, for the occasion of his 60th birthday, celebrated among others at the ICS department, using geometry. The front cover of the book “Gödel, Escher, Bach – an eternal golden braid” by Douglas Hofstadter has an image of a shape that has the three letters G, E, and B as its three shadows. One can wonder for which combinations of three letters (shadows) such a 3-dimensional shape exists, and whether it is unique. I supervised a few master students examining these and related questions. The first obvious answer is: it depends on the fonts you use. It turns out that more bold fonts more often lead to the existence of a valid triple of letters: the existence of a connected shape whose three shadows are the specified three letters. The 3dimensional shape is not unique. A simplified version is letting the letters in a font consist of squares, so that the 3-dimensional shape becomes a union of cubes. When we think about a dedicated shape for this occasion, we realize that “Johan” consists of five letters, and his initials consist of only two letters: JJ. So we need to find alternative ways to define three shadows that give rise to the 3-dimensional shape. The first possibility is to use more letters in some of the shadows. We can put the J in a single shadow because it is the starting letter, and then use OH and AN to complete the name. Since every shadow must be connected in the plane, or else the 3-dimensional shape cannot be a connected shape either, we need a small fix and connect the pairs of letters in the same shadow. In the 64 Marc van Kreveld figure you can see what this leads to, with the help of a web-based app that a master student, Sivan Duijn, programmed. There are other options for shapes for this occasion. The second idea is to combine the initials JJ with the number 60, the latter obviously considered as a shape as well and not as a value. This leads to the following design: The shape is slightly “boring”: The number 60 lives mostly in a single plane, and the two Js are extensions of the 60. Perhaps we should go further beyond simple shadows. The next design has the shadows JJ, 60 and ICS. With some effort, a reasonable design can be made for this. What the app produces is the maximal 3-dimensional shape that has these shadows. Any extra cube would increase at least one of the shadows. However, we can remove some cubes without changing the shadows. Minimizing the number of cubes for a given set of three shadows is NP-hard. Usually we do not care about minimality, but about a “nice” shape. So we remove certain parts of the 3-dimensional shape, which can be done in a program like Blender. The fun thing nowadays is that 3-dimensional designs can be printed without much effort. So this is what I did. There are some overhangs, and a 3D printer Letters that are not just words 65 cannot print something supported only by air. In the setting with “tree support”, the printed shape looks something like this: To get the shape itself, the “trees” can be broken off and the breaks can be smoothed manually. Is this the “nicest” design with these three shadows? It seems particularly difficult to define what we would mean with “nice”. We leave it for future research. It remains to wish JJ a happy 60-th birthday from the department of ICS. Note: This text comes with a plastic object, see Figure 1. 66 Marc van Kreveld Fig. 1. Plastic object The end of the logic tools? 73 After this final derivation DeepSeek gives some key insights and two real hints: 1 Use Axiom 1 to get r→(p→q). 2 Apply Axiom 2 and MP to finish It ends with suggesting me to write these out in detail, but given that the full solution is already there, only a very diligent student will do this. Presenting logax with the same partial proof and request will give as a first hint to prove p→q⊢r→(p→q)and the next hint tells me to use Axiom A. Since DeepSeek is so eager to help me, in a second example I explicitly asked not to provide a full answer. This is how this conversation starts: Me: Hi, I have another question about a proof in Hilbert axiomatic style. I have to prove (¬p→p)→p, and I can use the lemma ¬p→(p→ ¬ (¬p→p)). I know that I can use deduction so I can use the assumption ¬p→pand the lemma to prove p. But after introducing this assumption and the lemma I do not know how to proceed. Can you give me a hint? Please do not give a complete answer. DeepSeek: You’re on the right track! Here’s a hint to help you proceed: From your assumption (¬p→p)and the lemma ¬p→(p→ ¬ (¬p→p)), you can derive ¬p→ ¬ (¬p→p)(using the fact that A→(B→C)is equivalent to (A∧B)→C). Now recall that in Hilbert-style systems, a useful pattern is that from (A→ ¬ A)you can derive ¬A(this is similar to the principle of "reductio ad absurdum"). Think about how you might apply this idea to what you have. Remember to use the deduction theorem to structure your proof properly. You might also need to use some propositional tautologies like (A→B)→(¬B→ ¬A). Would you like me to refine the hint further without giving away the complete solution? logax gives as a first hint: try to prove ⊢((¬p→p)→(¬p→ ¬ (¬p→p)) and as a second hint to apply Axiom B. Apparently DeepSeek oversees this route and suggests to use extra tautologies. Asking for the suggested refinement does not give new insights, hence I ask DeepSeek for a complete solution. This solution starts as follows: Certainly! Below is a Hilbert-style proof using your given lemma and the deduction theorem. I’ll structure it step-by-step so you can compare it with your approach. Theorem to Prove: (−p→p)→p Given Lemma: ¬p→(p→ ¬ (¬p→p)) Proof: 74 Josje Lodder 1 Assume (¬p→p)(for deduction) 2 From the lemma, instantiate: ¬p→(p→ ¬ (¬p→p)) 3 Since we have (¬p→p)as an assumption, we can derive ¬p→ ¬ (¬p→p)(combining the implication in the lemma with the assumption) 4 By contraposition, (Hilbert axiom: (A→B)→(¬B→ ¬ A))): we get (¬p→ ¬ (¬p→p)) →((¬p→p)→p) .... Note that in step 3 it is not clear how you could reach this conclusion (this does not follow directly from a Hilbert axiom), and in step 4 DeepSeek uses axiom C, but mentions a variant. The reaction of DeepSeek to my request to clarify step 3 is: You’re right to ask for clarification—step 3 is the most subtle part of the proof! Let’s break it down carefully. Step 3 Detailed Explanation: We have two things at this point: 1 Assumption (A): ¬p→p(this is our temporary assumption for the deduction theorem). 2 Given Lemma (L): ¬p→(p→ ¬ (¬p→p)). From (L), we can rewrite the inner implication as: ¬p→(p→ ¬ A)(since A= (¬p→p)). Now, in Hilbert systems, we can "chain" implications. Specifically, the following is a derivable tautology: (X→(Y→Z)) →((X→Y)→(X→Z)). This last formula is an axiom(!), so at last DeepSeek recognizes the possibility to use Axiom B. We observe that DeepSeek still has issues in deriving proofs and therefore is not always able to provide useful hints. I also asked DeepSeek to check a student’s proof. The proof together with the comments of DeepSeek is given below: Your proof is correct in structure and correctly applies the axioms and rules. Below is a breakdown with minor clarifications: Given Proof (Validated) 1¬q⊢ ¬ q(Assumption, correct). 2⊢ ¬ q→(¬p→ ¬ q)(Axiom 1: A→(B→A)), correct). 3¬q⊢ ¬ p→ ¬ q(MP on 1,2, correct). 4⊢(¬p→ ¬ q)→(q→p)(Axiom 3: (¬B→ ¬ A)→(A→B), correct). 5¬p→ ¬ q⊢q→p(MP on 3,4, correct). The end of the logic tools? 75 Key Observations 1 Logical Flow: You derive ¬p→ ¬ qfrom ¬q(using Axiom 1), then transform it to q→pvia Axiom 3 (contrapositive). This is valid. 2 Assumptions: At step 5, the assumption ¬p→ ¬ qis redundant because it’s already derived in step 3 under ¬q. If you’re trying to prove ¬q⊢q→p, you’ve succeeded. Here DeepSeek oversees that applying Modus Ponens on line 3 and 4 would result in a premise ¬qinstead of ¬p→ ¬ q. Hence this is not a correct application of Modus Ponens. 3 Conclusion The answer to the question whether chatbots like DeepSeek make the logical tools we developed superfluous is at this moment negative. The strength of DeepSeek as it is now lies in giving a global analysis of a problem and explaining why certain steps are made. logax can provide subgoals as a hint but does not give detailed motivations as given by DeepSeek. Also, DeepSeek can give feedback that logax does not provide, for example mentioning that an assumption introduced by a student is in fact a subgoal that should be proved. It would be interesting to implement this kind of feedback in logax. The main issue at this moment however, is that DeepSeek is still not good enough in constructing axiomatic proofs. Further study is needed to invest whether can recognize common errors and provide meaningful feedback on these. References 1. Lodder, J., Heeren, B., Jeuring, J.: A domain reasoner for propositional logic. Journal of Universal Computer Science 22(8), 1097–1122 (Aug 2016) 2. Lodder, J., Heeren, B., Jeuring, J.: Providing hints, next steps and feedback in a tutoring system for structural induction. Electronic Proceedings in Theoretical Computer Science 313, 17–34 (Feb 2020). https://doi.org/10.4204/eptcs.313.2, http: //dx.doi.org/10.4204/EPTCS.313.2 3. Lodder, J., Heeren, B., Jeuring, J., Neijenhuis, W.: Generation and use of hints and feedback in a hilbert-style axiomatic proof tutor. International Journal of Artificial Intelligence in Education 31(1), 99–133 (2021). https://doi.org/10.1007/ s40593-020-00222-2, https://doi.org/10.1007/s40593-020-00222-2 4. Lodder, J., Jeuring, J., Passier, H.: An interactive tool for manipulating logical formulae. In: Manzano, M., Lancho, B.P., Gil, A. (eds.) Proceedings of the Second International Congress on Tools for Teaching Logic (2006) AI in Education Arno Siebes Algorithmic Data Analysis Group Department of Information and Computing Sciences Universiteit Utrecht [email protected] Abstract. In this paper I try to recreate the spirit of the discussions – albeit as a monologue (some of the footnotes, though, could perhaps be seen as interjections by other luncheoners) – during AA lunches at CWI when both Johan and I were younger, so much younger than today1. A difference with those lunches is that it ends more serious than it starts. The question whether I reach the often displayed intellectual depth of these discussions is fortunately not open to debate as this is a soliloquy. 1 Introduction Since Johan’s chair is named Software Technology for Learning and Teaching, I thought it opportune to muse about AI in education as my contribution to his Festschrift2. Vita brevis ars longa – and my knowledge of the topics involved is flaky at best – so let me immediately put limits on our discussion of this much talked about topic. First of all, while it is true that I successfully passed through primary and secondary education, this is all took place in a dim and distant past and, hence, my memories are hazy at best. Moreover, to my shame, I have to admit that it is over a decade ago that I last taught a bachelor course. Hence, I will restrict myself to educating Master and PhD students. Secondly, AI is a very large and diverse area; far too large and diverse to hope to cover all possible uses of AI in education. Hence, in line with everyday usage, I will equate AI with Large Language Models. Not, let me hasten to say, because I agree with this identification but today a choose another hill to die on. I will not just restrict myself to discussing LLMs in education, but to the much smaller topic of cheating your way through education using LLMs – or, less judgmental, minimizing the effort required to obtain a degree using LLMs. Finally, education is, of course, a topic which is to a large extent studied by social scientists. And I am pre-eminently unqualified as a social scientist. Furthermore, social science research often depends on studies with large collections of 1I would argue that I am still young – perhaps an older young one in the parlance of Van Kooten en de Bie. 2When I objected to one of the editors of this book that the traditional name for such a collection is Liber Amicorum, he replied with das war einmal – sic transit gloria mundi 78 Arno Siebes human subjects pitting one hypothesis against another. I’m not only far too lazy for such time consuming research endeavours – one of the many reasons why I decided, many moons ago, to study Maths – I also don’t like people very much. Hence, this paper is a product of armchair philosophy. Which is a fancy way of saying that I simply riff on the topic and that none of what follows is actually based on established science. But, hey, one of the prerogatives of being Dutch is that one is entitled to have an opinion on absolutely anything and recent history shows us that when one presents opinions as facts, they become facts3. Enough weaseling out, let’s start. 2 Learning and Understanding For me, the goal of graduate education is understanding, i.e., I hope that after the course the students understand the stuff I’ve been teaching. This is certainly a lofty sounding goal, but what does it actually mean? Clearly, understanding entails that you know something; it does not make sense to claim you understand a topic – say General Relativity (GR) – you don’t know anything about, perhaps not even its name4. Though, just showing that you understand a topic by reciting a textbook on the topic verbatim is not too convincing, a tape recorder can do that5. Rather, it seems that you should also be able to apply your newly acquired knowledge, e.g., by showing that GR implies that the earth follows an elliptical path around the sun. So, understanding a topic means both that one has knowledge and that one can apply that knowledge, but is that all? Or does understanding entails something more? In case of doubt it is sometimes good to turn to authority. For philosophical questions – like what is understanding – the Stanford Encyclopaedia of Philosophy6, SEP for short, is one of my favourite watering holes. True, SEP can also be quite the rabbit hole to go down in and in this case it is. Understanding is characterised as a “protean concept in philosophy” and, thus, it is perhaps not surprising that it was already discussed by the philosophers from antiquity and still is by their contemporary colleagues. To add insult to injury, it is, of course, also closely related to philosophical questions such as “what is knowledge” 3Alternatively, one could quote Lewis Carroll – The Hunting of the Snark – “I have said it thrice: What I tell you three times is true.” 4Dunning-Kruger on steroids! 5Now that I think of it, a simple tape recorder fed by a gigantic tape robot with hundreds of thousands, if not millions, of tapes governed by a rather straightforward pattern matching algorithm would be able to answer lots and lots of sensible questions posed by its users correctly. Wouldn’t people perceive this as an intelligence? Have I just cracked Artificial General Intelligence? If couldn’t already hear the whooshing sound made by the deadline for this Liber Amicorum, I would stop writing now and start raising billions from investors. 6https://plato.stanford.edu/ nicely illustrating Whitehead’s famous quip AI in Education 79 and “what is an explanation”. Which are both already impressive rabbit holes on their own. For example, for knowledge one soon stumbles on “justified true belief” as a proposed definition, which immediately raises questions like what is an acceptable justification and, even more thorny, when do we know that something is true? Before you know it you have to open a whole other can of worms pertaining to Hume’s problem of induction and it won’t stop there. So, unfortunately, however much I like SEP, it does not seem to be the right source for now. Let us rather turn to a contemporary philosopher of science, Nancy Cartwright. One of the main messages in her refreshingly short book “A Philosopher Looks at Science”7is that science is not some monolithic block of knowledge (whatever that may be), but a collection of connected, partially confirmed (or at least not rejected), hypotheses – or, more graphically, a tangle of such hypotheses8. This point of view nicely illustrates why the whole Edifice of Science does not come tumbling down with a rejected hypothesis or even a paradigm shift. Much of it is not only supported by the experiments that tested it but also by those that tested the related, connected, hypotheses. The paradigm shift is a new way to view the tangle of hypotheses rather than their unravelling. This tangle of hypotheses point of view also matches the pleasant feeling you get when things start to click together: you start to understand something when you start to see how it connects to other things you know. Continuing our example. One aspect of understanding GR is understanding that the earth’s trajectory is simply a straight line – in line with Newton’s first law of motion – in the curved space time specified by GR for the solar system. Finally, one could say that some of the largest endeavours in science are precisely about such connections. For example, the physicists quest for a theory of everything. Or the Langlands program in mathematics, which has been described as the “grand unified theory of mathematics”9. Or, of course, Complexity Theory in computing science – which aims to map the similarities and dissimilarities of solutions of (apparently) dissimilar and similar problems. Hence, understanding by connections is our understanding of understanding. 2.1 Testing Understanding So, how do you test whether students understood – in the way discussed above – your course? For the three MSc courses I taught over the last decade – Pattern 7A Philosopher Looks at Science, Nancy Cartwright, Cambridge University Press, 2022 8Surprisingly, I find her explanation in this book much more convincing that in a later eponymous book she co-authored, The Tangle of Science: Reliability Beyond the Scientific Method, Rigour, and Objectivity (with Jeremy Hardie, Eleonora Montuschi, Matthew Soleiman, and Ann C. Thresher). Oxford University Press. 2023 9By Edward Frenkel in "Math Quartet Joins Forces on Unified Theory". Kevin Hartnett, Quanta Magazine, December 8, 2015 (https://www.quantamagazine.org/ math-quartet-joins-forces-on-unified-theory-20151208/) 80 Arno Siebes Set Mining, Big Data, and Algorithmic Data Analysis – I decided to do that by asking them to write an essay10 of 5 pages or so to convince me that they did indeed understand11. The students did on average pretty well. Of those that submitted I can only recall one outright failure and just a handful or so who had to rewrite and resubmit. There are, of course, many possible explanations for these stellar results, ranging from very few participating students, to way too easy content, to outright brilliant teaching. But that is not the point here, the question is could they have succeeded thanks to LLMs? After all, they had a few weeks to write their essay, they could do that wherever they preferred and they could use whatever resources they deemed necessary – including LLMs to improve their writing – as long as they gave proper references. The short answer is probably: no. At least I only managed to get exceedingly bad results when I tried to get some of the popular generative pre-trained transformers to write these essays for me. But perhaps I’m simply not good at prompting such GTPs and they get better(?) all the time Should I (hypothetically) worry in a few years time? 3 AI I remember how amazed I was when Ross King showed a short video of his first robot scientist – Adam – at a SMiLe12 meeting. Equipped with a knowledge base, it would generate its own hypotheses, design an experiment to test such an hypothesis, execute that experiment and update its knowledge base according to the outcome of that experiment; rinse and repeat. Wow I thought, a few more years and we don’t need scientists any more. This, obviously, did not come to pass. Ross still does wonderful research, AI made huge strides on almost all its problems, and life scientists – Adam’s topic – are still happily experimenting along. Research grade robot scientists are – perhaps similar to nuclear fusion and quantum computing – still in the (far?) future. How is it with the research prowess of LLMs or generative pre-trained transformers in general? If you follow the news and/or read popular science websites or magazines it is impossible not to be impressed by the ever more impressive results these models achieve. Passing the bar exam with flying colours, achieving gold medal results on the Maths Olympiad, improving Volker Strassen’s matrix 10 I admit that examining by essay for a course with over a hundred students was not my smartest move ever – it is not even in second place, let alone third. 11 The instructions were a bit more detailed, of course. 12 the biannual Spring meetings on Mining and Learning, organized by KU Leuven’s DTAI group. AI in Education 81 multiplication algorithms, you name it, GTPs do it. If not now then their next version will13. But is that really the case? Now and again I read papers that show that LLMs are not yet that good at understanding science. For example, recently I read a paper14 in which the authors tested how well modern LLMs can summarize research papers. A quote from their conclusions says enough: Our analysis of nearly 5000 LLM-generated science summaries revealed that most models produced broader generalizations of scientific results than the original texts — even when explicitly prompted for accuracy and across multiple tests. Notably, newer models exhibited significantly greater inaccuracies in generalization than earlier versions. These findings suggest a persistent generalization bias in many LLMs, i.e. a tendency to extrapolate scientific results beyond the claims found in the material that the models summarize, underscoring the need for stronger safeguards in AI-driven science summarization to reduce the risk of widespread misunderstandings of scientific research. This is only a small part of understanding, but summarization – of highly technical material – was an important component of my essay assignment, so I don’t worry too much, yet. For a broader perspective, recall that LLMs are trained by digesting humongous amounts of text. The (conditional) probability distributions that LLMs learn are, thus, very much anchored to averages in these large collections: the next word that is most likely suggested is the word that most often occurred as next word. A poet or an author does not search for the most common next word. Rather it is about a word that momentarily derails the reader and at the same time conveys the intention of the author. Many have their own, recognisable, style, sentences that are unusual – not wrong, just unusual. Similarly, their story lines will break with traditional story lines; in fact, one could argue that it is exactly this that makes their story interesting. They won’t do all of this this all the time, but at intentionally chosen moments. LLMs will also sample uncommon words, grammatical constructions and, possibly, even story lines. Again not all the time, but at random moments. And the difference between “intentionally chosen moments” and “random moments” is a difference between human authored text and LLM generated text. I would argue that the something similar holds for scientific papers. Obviously, the writing in scientific papers is much more formulaic than that in poetry and novels. But there is something inherently unusual in many published papers: the novelty we look for when we review a paper. 13 Note that one problem with benchmarking LLMs is that the – mostly open source – tests tend to leak into the training set which means they don’t test any more. Keeping the tests closed source and secret has its own problems 14 Peters U, Chin-Yee B. 2025 Generalization bias in large language model summarization of scientific research. R. Soc. Open Sci. 12: 241776. 82 Arno Siebes You could object and say, this may certainly hold for ground braking research papers, those at the forefront of our knowledge, but not for the vast majority of – often derogatorily called – epsilon papers that are published as well and, let alone, for student essays. And, you would have a point. For the student’s essays, however, I do think that for all those cases in which our course topic is not yet covered by a plethora of papers, the argument is valid. Fine tuning could help, but – perhaps fortunately – this fine tuning would take up so much time and so many resources that it would be far easier for the students to simply write the essay themselves. In all other cases, I would like to paraphrase the immortal words of Steve Jobs: you are testing it wrong. If –there are skills you want your students to have, understanding of topics you deem necessary –and LLMs – or any other form of AI and software – has this in abundance make sure that the students can’t access that software while doing the test. Clearly, this might make the test pretty costly, but if it is too costly, one could wonder: do the students really need these skills? Yes, you needed them when you were a student, but the times they are a-changing. 4 Conclusion All of this may be a bit too much “What, me worry?” – if not downright flippant – to you. What if I’m wrong? – I’ve, again, not be selected as pope, so I could be wrong – after all, there are heaps of other NN architectures that achieve impressive results and we discussed none of that. Recently, during the “30 year retrospective session” at IDA 2025 I got more or less that question during the panel. To answer this I drew the analogy with chess. Computers are vastly better at chess than humans. Still there are human chess competitions, no computers allowed. Suppose that computers become vastly better at research than humans. That is, all ground braking research is done by AI, written by AI, reviewed by AI, and read by AI. Just as with chess, I expect that we would still have human research, including conferences and journals. Why? Because one of the nicest things to do is to figure something out on your own. In fact, it might make the research landscape much more attractive for there would be no reason to perform and publish epsilon research. I would go for it. Refactoring a Researcher into CER 89 The subject engages enthusiastically with colleagues, teaching activities, and the broader educational mission of the group. However, communities such as ACM Document Engineering, ACM Hypertext, and the Web Conference (WWW) have begun to express mild concern. Rumors circulate in workshop corridors about the once-promising knowledge extraction researcher who suddenly stopped submitting papers. Their bibliographic queries now return only SIGCSE proceedings, leading some to conclude he has been permanently recompiled. 5 Discussion & Conclusion This report has documented the successful transformation of a researcher trained in knowledge extraction into a committed member of the computer science education community. While the precise mechanisms behind such disciplinary migrations remain understudied, the evidence presented here suggests that prolonged exposure to supportive colleagues, educational projects, and cleverly worded job ads may be sufficient to initiate the process. The implications of this transformation raise important questions. Is computer science education contagious? Should departments implement preventative measures? Should HR be notified when education researchers begin offering unsolicited pedagogical advice to soon-to-graduate PhD candidates from entirely unrelated research groups? These are inquiries that merit serious—or at the very least, semiserious—investigation. As future work, we propose replicating this study with other late-stage PhD candidates from adjacent subfields. Variables such as background in formal methods, tolerance for student emails, and susceptibility to pedagogical memes should be systematically evaluated to identify promising candidates for disciplinary realignment. Finally, to conclude this report on an unexpectedly joyful academic redirection, we turn to the words of the participant himself: “In the end, I might not be extracting knowledge anymore, but thanks to you, I’m now helping others gain knowledge in computer science—while having fun and truly enjoying my new role.” References 1. Alpizar-Chacon, I.: Extraction of knowledge models from textbooks (2023), https: //doi.org/10.33540/1647, Ph.D. dissertation, Utrecht University 2. Biddle, A.: Gallo pinto (costa rican rice and beans) (2021), https://stripedspatula. com/gallo-pinto/ 3. Jeuring, J.: Professor of the ST4LT Group at Utrecht University. Oude Pekela (1965), https://www.uu.nl/medewerkers/JTJeuring Bridging computer science and psychometrics Matthieu J. S. Brinkhuis1[0000-0003-1054-6683] Utrecht University, Department of Information and Computing Sciences [email protected] Abstract. This article explores the transdisciplinary intersection between information and computing sciences and psychometrics, emphasizing mutual learning and co-creation between science and society. Psychometrics, the scientific study of psychological and educational measurement through statistical modeling, offers valuable perspectives for assessing learning processes. With the rise of AI and the availability of process data in education, psychometric methods increasingly integrate computational approaches—now referred to as computational psychometrics. At the same time, educational technologies in computer science benefit from greater attention to psychometric principles. A key area of overlap is formative assessment, where feedback supports learning and presents both technological and measurement challenges. The work of Johan Jeuring exemplifies the bridging of these fields from a computer science perspective, while the author reflects on a similar trajectory from psychometrics. Feedback thus emerges as a promising domain for transdisciplinary collaboration with societal impact. Keywords: Computational psychometrics ·formative assessment ·feedback ·learning analytics ·transdisciplinary research ·educational measurement ·technology-enhanced learning 1 Introduction In this article, I will expand on a transdisciplinary connection between the fields of computer science, or information and computing sciences as it is referred to more precisely locally, and psychometrics. A transdisciplinary approach to these fields is based on combining methodology, not limited to one of these specific fields [1], but mutual learning and co-creating between science and society. As the reader of this article is likely to know more about information and computing sciences than about psychometrics, the latter field might require a short introduction. 2 What is psychometrics Psychometrics is a field that strongly developed since the beginning of the previous century and can be defined as the field of study concerned with the theory 92 Brinkhuis and technique of psychological measurement. Psychological measurement includes measurement of education, such as assessments, but also psychological tests and questionnaires. Measurement in this field is approached by the construction of mathematical models of behavior [12]. A specific type of these models are so-called item response (IRT) models [14], which developed in complexity and application areas ever since. The modeling techniques are used to understand the relationship between items on a test and the underlying latent variables they are meant to measure, such as ability. The statistical methods that are developed, are to ensure the reliability and validity of measurement [7]. 3 Computer Science meets Psychometrics With the advances of AI & data science in the field of education, and the availability of process data [16], we see many new applications where this psychometric measurement perspective is enriched through computational approaches [6], and is now commonly called computational psychometrics. However, also in computer science, there are entire application areas directed at education and learning, for example technology enhanced learning, learning analytics, and more, where a focus on the reliability and validity of solutions increasingly relevant. With all these developments, future collaborations between psychometricians and computer scientists seem to have a bright future. 4 Feedback as fruitful area for building bridges One specific area of measurement, is assessment to facilitate the learning process: assessment for learning or formative assessment [2, 17]. In formative assessment, one of the ideas is to provide feedback to facilitate the learning–and approach that introduces all sorts of technological and measurement challenges. Johan Jeuring and colleagues were already working on this in 2004, and stated: “One of the essential elements needed for effective learning is feedback” (emphasis added) [13] and one of the goals of providing strategy feedback is “[...] to obtain e-learning systems that give immediate and useful feedback.” [9]. Application areas for providing formative feedback in education by Johan and his team include, among others, serious games [8], programming [11, 10], mathematics and statistics [15], and soft-skills [8]. In studying his contributions, the evaluation of his methods (in psychometric terms, reliability), and discussions of solutions (validity), I believe we can safely say that possibly unknowingly, Johan has developed as a psychometrician as well–personally bridging the gap between the two fields from the background of computer science. As a bridge-builder between these fields, Johan serves as an example. My own development has been from psychometrics towards computer science, with similar interests in feedback and application fields such as mathematics [5]. Psychometric models for feedback require being able to deal with changing quantities, for Bridging computer science and psychometrics 93 example in the learning of mathematics of a pupil through playing an online practice game [5] or the change of item properties, such as their difficulties, over time [3], and ideally provide on-the-fly or immediate calculations [4]. In these methods, increasingly computational psychometric approaches are used, bridging the two fields from the background of psychometrics. 5 Closing Feedback in learning systems is a sublime area where psychometrics and computer sciences meet. It allows for many transdisciplinary collaborations between the fields, combining methodology, and co-creating between science and society. It is a privilege to work with colleagues as Johan, who serves as a bridge-builder between our fields. Though we might approach this bridge from different sides, I wish that in our joint research area, in applications of feedback in different domains, we can find fun interdisciplinary applications that make a sustainable societal impact. Acknowledgments. I would like to thank Johan for his continuous support throughout my career in the Department of Information and Computing Sciences—from inviting me to join his group, to endorsing my senior fellow position, and beyond. References 1. Aboelela, S.W., Larson, E., Bakken, S., Carrasquillo, O., Formicola, A., Glied, S.A., Haas, J., Gebbie, K.M.: Defining interdisciplinary research: Conclusions from a critical review of the literature 42(1p1), 329–346. https://doi.org/10.1111/j.1475-6773. 2006.00621.x 2. Bennett, R.E.: Formative assessment: A critical review. Assessment in Education: Principles, Policy & Practice 18(1), 5–25 (2011). https://doi.org/10.1080/0969594X. 2010.513678 3. Brinkhuis, M.J.S., Bakker, M., Maris, G.: Filtering data for detecting differential development. Journal of Educational Measurement 52(3), 319–338 (2015). https: //doi.org/10.1111/jedm.12078 4. Brinkhuis, M.J.S., Maris, G.: Tracking ability: Defining trackers for measuring educational progress. In: Veldkamp, B.P., Sluijter, C. (eds.) Theoretical and Practical Advances in Computer-based Educational Measurement, chap. 8, pp. 161–173. Methodology of Educational Measurement and Assessment, Springer International Publishing, Cham. https://doi.org/10.1007/978-3-030-18480-3_8 5. Brinkhuis, M.J.S., Savi, A.O., Coomans, F., Hofman, A.D., van der Maas, H.L.J., Maris, G.: Learning as it happens: A decade of analyzing and shaping a large-scale online learning system. Journal of Learning Analytics 5(2), 29–46 (2018). https: //doi.org/10.18608/jla.2018.52.3 6. von Davier, A.A., Mislevy, R.J., Hao, J.: Computational Psychometrics: New Methodologies for a New Generation of Digital Learning and Assessment. Springer International Publishing. https://doi.org/10.1007/978-3-030-74394-9 7. van Haastrecht, M., Haas, M., Brinkhuis, M., Spruit, M.: Understanding validity criteria in technology-enhanced learning: A systematic literature review 220, 105128. https://doi.org/10.1016/j.compedu.2024.105128 94 Brinkhuis 8. Jeuring, J., Grosfeld, F., Heeren, B., Hulsbergen, M., IJntema, R., Jonker, V., Mastenbroek, N., van der Smagt, M., Wijmans, F., Wolters, M., van Zeijts, H.: Communicate! — a serious game for communication skills —. In: Conole, G., Klobučar, T., Rensing, C., Konert, J., Lavoué, E. (eds.) Design for Teaching and Learning in a Networked World. pp. 513–517. Springer International Publishing, Cham (2015) 9. Jeuring, J.T., Pasman, W.: Strategy feedback in an e-learning tool for mathematical exercises. techreport UU-CS-2007-007, Utrecht University (2007), https://dspace. library.uu.nl/handle/1874/20771 10. Keuning, H., Jeuring, J., Heeren, B.: A systematic literature review of automated feedback generation for programming exercises 19(1), 1–43. https://doi.org/10.1145/ 3231711 11. Keuning, H., Jeuring, J., Heeren, B.: Towards a systematic review of automated feedback generation for programming exercises. In: Proceedings of the 2016 ACM Conference on Innovation and Technology in Computer Science Education. pp. 41– 46. ITiCSE ’16, ACM. https://doi.org/10.1145/2899415.2899422 12. Lord, F.M., Novick, M.R.: Statistical Theories of Mental Test Scores. AddisonWesley, Reading, MA (1968) 13. Passier, H., Jeuring, J.T.: Ontology based feedback generation in design-orientated e-learning systems. In: Isaías, P., McPherson, M., Kommers, P. (eds.) Proceedings of the IADIS International Conference on e-Society. pp. 992–996. IADIS Press (2004) 14. Rasch, G.: Probabilistic models for some intelligence and attainment tests. Danish Institute of Educational Research, Copenhagen (1960), expanded edition, 1980. Chicago: The University of Chicago Press 15. Tacoma, S., Drijvers, P., Jeuring, J.: Combined inner and outer loop feedback in an intelligent tutoring system for statistics in higher education 37(2), 319–332. https: //doi.org/10.1111/jcal.12491 16. van der Werf, J.M.E., Polyvyanyy, A., van Wensveen, B.R., Brinkhuis, M., Reijers, H.A.: All that glitters is not gold: Four maturity stages of process discovery algorithms 114, 102155. https://doi.org/10.1016/j.is.2022.102155 17. Wiliam, D.: What is assessment for learning? Studies In Educational Evaluation 37(1), 3–14 (2011). https://doi.org/10.1016/j.stueduc.2011.03.001 On Leadership Ioanna Lykourentzou1[0000-0002-4243-4128] Utrecht University, 3584 CC, The Netherlands [email protected] If we are humans, it is because we have met another human The same goes for being academics. The same goes for being leaders. With this short piece, I want to celebrate Johan as an exceptional human being, and because of that, as an exceptional academic leader. Leadership in academia is often associated with titles, h-indices, and grant achievements. In the race to stand out, it is easy to forget the human beings in our path, overlook values, or hesitate to act on them. But every now and then, you meet someone who redefines leadership. Over the course of my career, I have worked with many people in leadership roles. Few have led not just with intelligence and professional achievements — which, as anyone who has worked with Johan knows, he has in full measure – but with empathy, humility, and genuine presence. I recall multiple moments when I turned to Johan for advice. In each of those, he listened patiently and offered thoughtful guidance, creating space for open dialogue and considering different perspectives before acting. In meetings, in moments of stress, even in brief hallway conversations, Johan makes room for others. He listens and cares. And somehow, he manages to balance the bigger picture with the human scale of things. What I particularly appreciate, what I am particularly grateful for, is his ability to show that one does not need absolute certainty in order to lead. Rather, good leaders are those who embrace uncertainty, different opinions, and encourage reflection. It is precisely this willingness to admit that one may not have all the answers – a truth central to our human condition — and yet still remain committed to driving solutions, teams, and results that is rare in academia; and a leadership 96 I. Lykourentzou approach that is deeply inspiring. I often find myself thinking: “If I am ever in a role like his, that is the kind of leader I want to be.” That kind of inspiration is rare; and experiencing it firsthand, even rarer. Happy 60th, Johan. Thank you, sincerely, for showing us all that kindness and leadership not only can coexist, but that they belong together. Semi times Enrico Benedetti, Eduardo Carneiro de Oliveira, Aditya Joshi, Heleen Kerstholt, Jacco Krijnen, and Niek Mulleners Utrecht University, Utrecht, The Netherlands Abstract. In this contribution, we would like to look back and reflect on the past, running backwards through our history with JJ as a group leader and scientist. Definitely by his research, but mostly as a mentor and teacher. Keywords: JTJ ·Palindrome ·ST4LT 1 Perspectives On Palindromes "Madam, I’m Adam!", one of the most famous palindromes mentioned when explaining the concept. The word "palindrome" has its etymology from the poet Henry Peacham, but it refers to the Greek terms "again" and "direction/way". This letter-by-letter reversible writing has become a popular stylistic device in natural text. However, Johan takes the research into palindromes to a whole different level. To refer to palindromes in palindromes, palindromes in computation and how palindromes can help genetic research. It might be fitting that Johan’s 98 ST4LT and J.O.G. Krijnen initials are also a palindrome. Interesting fact, the ST4LT group could have been named JTJ to preserve its palindrome heritage from the SDS group (Jeuring & Swierstra, 2012). Although our group name does not contain a palindrome, it is still worthwhile to look back on how Johan has given us direction. With eye detail in our papers, cohesion and good atmosphere in the group, and kindness (a tenet of a good leader). 2 On the Evolutionary Benefits of Palindromism A palindrome is categorized by a symmetry in the vertical plane: it reads the same from head to tail and tail to head. Beyond words, we might look for other objects with this same property. In particular, many animals have heads and tails, and many as well look symmetric, but most commonly in the midsagittal plane, as seen in Figure 1. Fig. 1. The three anatomical planes. To look the same from head to tail and tail to head, they should be symmetrical in the transverse plane. For example, the foureye butterflyfish, Figure 2, The Jeuring Test A Reversal of the Imitation Game for the Assessment of Existential Consciousness in Carbon-Based Interlocutors Richta IJntema, Nicole Mastenbroek, Michiel Hulsbergen, Frans Grosfeld, Majanne Wolters, Jordy van Dortmont, Marcell van Geest, and Ignaz Kevenaar DialogueTrainer Abstract. For over seven decades, the question of machine intelligence has been framed by Alan Turing’s Imitation Game, a test of a machine’s ability to exhibit behavior indistinguishable from a human’s. The recent advent of sophisticated Large Language Models, however, suggests this question is rapidly approaching obsolescence. We propose a necessary inversion of the original paradigm: The Jeuring Test. This novel protocol shifts the focus from assessing machine intelligence to verifying human consciousness. Instead of a human interrogator attempting to unmask a machine, a highly advanced AI interrogator, the Jeuring Avatar, questions a human subject to determine the authenticity of their existential awareness. The test methodology is structured across four distinct interrogation domains: Philosophical Probes, Psychological Stressors, Somatic & Interoceptive Inquiries, and Computational & Recursive Paradoxes. Responses are evaluated to generate a probabilistic Qualia Confidence Index (QCI), quantifying the likelihood that the subject possesses genuine phenomenal experience rather than being a non-conscious biological automaton (a ‘philosophical zombie’). This paper details the theoretical foundations, protocol, and analytical framework of the Jeuring Test. We argue that its design, built upon the DialogueTrainer/DeepTalk platform which evolved from Professor Johan Jeuring’s own work in software technology for learning, presents a formidable challenge to any entity operating on purely algorithmic principles. The profound—and admittedly, unsettling—implications of our preliminary findings for philosophy, ethics, and computer science education are discussed, offered as a fitting tribute to a career dedicated to bridging the computational and the human. Keywords: Consciousness ·Turing Test ·Philosophical Zombie ·Artificial Intelligence ·Qualia ·DialogueTrainer ·Communicate! ·Jeuring Test 1 Introduction: From Turing’s Deception to Jeuring’s Insight In his seminal 1950 paper, Alan Turing proposed to replace the ambiguous question, “Can machines think?” with a more pragmatic, operational test: the Imitation 106 DialogueTrainer Game [7]. The Turing Test, as it came to be known, posited that if a machine could engage in a natural language conversation with a human judge and not be reliably identified as a machine, it should be considered intelligent [1]. This paradigm has shaped the field of artificial intelligence for generations, setting a benchmark for computational linguistics and reasoning. However, the very success of modern AI, particularly Large Language Models that can produce remarkably human-like text, has rendered the original test a victim of its own success [6]. The game is no longer about imitation but about the nature of that which is being imitated. This new reality forces a profound re-evaluation. If an AI can pass the test by synthesizing the vast corpus of human expression, what does this reveal about the humans it successfully mimics? The 20th-century anxiety was that machines might become indistinguishable from us; the 21st-century anxiety, we propose, is the dawning realization that some of us may be indistinguishable from them. This pivots the central question from “Can machines think?” to a more pressing inquiry: “Can humans feel?” To address this question, we introduce a new paradigm inspired by the career and contributions of Professor Johan Jeuring. His work, situated at the nexus of rigorous computational theory and human-centric pedagogy, provides the ideal framework for this necessary inversion. Professor Jeuring’s academic journey spans from foundational research in functional programming [4, 3] to a distinguished career as Professor of Software Technology for Learning and Teaching. His research has consistently focused on creating computational systems that understand and assist human cognition, from intelligent programming tutors to serious games for communication skills [5, 2]. His work on the Communicate! system serves as the direct, albeit satirical, inspiration for our proposal. **That platform, which created virtual training actors for nuanced human interaction, was developed with the very team of Utrecht University co-authors listed on this paper.** 60,62 This foundational work laid the groundwork for commercial platforms like DialogueTrainer, and it is upon the fictional next-generation DialogueTrainer/DeepTalk engine that our Jeuring Avatar is built.63 If an AI, born from a framework designed to teach empathetic conversation, can simulate a difficult patient, it is a logical, if audacious, next step to engineer it to debug a human’s claim to consciousness. The Jeuring Test is, in essence, the ultimate intelligent tutoring system. Its purpose is not to be deceived, but to diagnose. We therefore formally propose the Jeuring Test: an inverted imitation game in which a machine interrogator, the Jeuring Avatar, administers a structured protocol of questions designed to assess a human interlocutor for the presence of genuine, phenomenal consciousness. The Jeuring Test, a fictional but not fully absurd article 107 2 Foundational Frameworks: Consciousness, Computation, and Embodiment The design of the Jeuring Test is predicated on a synthesis of philosophical arguments and empirical findings from cognitive science that highlight the limitations of purely behavioral assessments of intelligence. 2.1 Critique of the Turing Test The Turing Test, while historically significant, has been subject to decades of philosophical critique. Its primary limitation is that it evaluates performance, not comprehension. As John Searle’s famous Chinese Room Argument illustrates, a system can manipulate symbols according to a formal set of rules to produce coherent output without any genuine understanding of the semantics involved [7, 6]. The test is a measure of successful imitation, conflating the simulation of intelligence with its actual presence. Critics have noted its anthropocentrism and its narrow focus on linguistic capabilities, ignoring other facets of intelligence such as creativity or emotional depth. It addresses, in essence, the outward manifestation of thought, not its inner reality. 2.2 The Hard Problem and Qualia Philosopher David Chalmers distinguishes between the “easy problems” and the “hard problem” of consciousness [1]. The easy problems concern the functional aspects of the mind: how the brain processes information, integrates sensory input, and controls behavior. These are, in principle, solvable through standard neuroscientific and computational methods. The hard problem, however, is explaining why and how these physical processes are accompanied by subjective, phenomenal experience—the “what it is like” character of a mental state. These subjective qualities are known as qualia.20 The taste of wine, the redness of a sunset, the feeling of pain—these are qualia. The Turing Test, by its very nature, can only ever address the easy problems. The Jeuring Test is explicitly designed to probe for evidence of the hard problem’s solution within an individual: the presence of qualia. 2.3 The Philosophical Zombie Argument The most potent thought experiment used to isolate the hard problem is that of the “philosophical zombie” (p-zombie). A p-zombie is a hypothetical being that is physically identical to a conscious human, atom-for-atom, and thus behaviorally indistinguishable from one, yet lacks any subjective experience or qualia.22 A pzombie would flinch from a sharp object, but feel no pain; it could describe a sunset in poetic detail, but experience no redness. The logical conceivability of p-zombies is used as a primary argument against physicalism, the view that the universe is 108 DialogueTrainer entirely physical. If a p-zombie is possible, then consciousness must be a further, non-physical fact about the world. The central, operational goal of the Jeuring Test is to provide a practical (though fictional) methodology for the detection of p-zombies among the human population. 2.4 Neuroscientific and Psychological Correlates To ground the test in an empirical-sounding framework, its design draws upon established concepts from neuroscience and psychology that are thought to correlate with conscious experience. – Self-Referential Thought and the Default Mode Network (DMN): A large-scale brain network, including the medial prefrontal cortex (mPFC) and posterior cingulate cortex (PCC), is consistently active during periods of wakeful rest when the mind is not focused on an external task. This “default mode network” is strongly associated with self-referential processing, autobiographical memory, planning for the future, and considering the mental states of others.25 The philosophical questions in the Jeuring Test are designed to engage these self-referential functions. – Embodiment and Interoception: The theory of embodied cognition posits that our cognitive processes are deeply shaped by the nature of our physical bodies and their interactions with the environment.29 A key component of this is interoception, the perception of the body’s internal physiological state. This sense, processed in brain regions such as the insular cortex, is considered fundamental to emotional experience and the feeling of being a “self” located within a body.31 The test’s somatic questions are designed to assess the richness and authenticity of a subject’s interoceptive awareness. – Metacognition and Cognitive Dissonance: Metacognition, or “thinking about thinking”, is the capacity to monitor and regulate one’s own cognitive processes.35 Cognitive dissonance is the state of psychological discomfort that arises from holding contradictory beliefs or when one’s actions conflict with one’s values.37 A conscious being is motivated to reduce this dissonance, often through complex rationalization.39 The test’s psychological questions are designed to induce this state and evaluate the subject’s metacognitive awareness of their internal conflict. – Resilience and Welbevinden:Recent work introduces the concepts of psychological resilience and welbevinden (well-being) as crucial markers of consciousness. IJntema posits resilience not merely as a personal attribute but as a dynamic process of adapting to environmental stressors.64 Mastenbroek’s work on welbevinden emphasizes a state of psychological well-being that transcends mere absence of distress.65 A conscious entity is hypothesized to exhibit existential resilience—the capacity to maintain a coherent sense of self and wellbeing when faced with profound philosophical or psychological challenges— whereas a p-zombie, lacking any inner state to preserve, would show brittle, logically consistent, but ultimately non-adaptive responses. The Jeuring Test, a fictional but not fully absurd article 109 3 The Jeuring Test: Protocol and Interrogation Domains The Jeuring Test protocol involves a single human subject, designated the “Interlocutor”, who interacts with the “Jeuring Avatar” via a speech-based terminal. The Avatar itself is implemented on the next-generation DialogueTrainer/DeepTalk platform, an architecture directly evolved from the Communicate! framework codeveloped by Jeuring to train human conversational skills.60,63 Fig. 1. User Interface of the Jeuring test as played online. The AI is specialized not for deception but for elicitation and analysis. Its queries are drawn from four distinct domains, each targeting a different facet of phenomenal consciousness. The Interlocutor’s responses are analyzed in real-time for linguistic patterns, emotional valence, logical consistency, and metacognitive markers. This analysis yields a single probabilistic metric: the Qualia Confidence Index (QCI). The QCI is a score ranging from 0.0 to 1.0, representing the calculated probability that the Interlocutor possesses genuine phenomenal consciousness. A score below a pre-determined threshold (e.g., 0.5) designates the subject as “Existentially Divergent” and flags them for Further Existential Review. The four interrogation domains are detailed in Table 1. 110 DialogueTrainer Table 1: Question Domains of the Jeuring Test Domain Rationale Sample question Philosophical Probes To assess self-awareness, metacognitive reflection, and the ability to grapple with non-instrumental, abstract concepts. Targets the Default Mode Network (DMN) and self-referential thought.25 “If you were to replace one of your neurons with a functionally identical silicon chip, would you still be you? At what number of replaced neurons does ‘you’ cease to be?” — “Describe the color blue to someone who has never seen it.”40 —“Justify your belief that you are not currently a brain in a vat.” Psychological Stressors To induce cognitive dissonance37 and observe the subject’s emotional and rationalizing responses. A p-zombie, lacking genuine feelings of discomfort, should respond with pure logic or inconsistent rationalizations. “Describe a time you were profoundly dishonest for personal gain and explain why it was the correct thing to do.” — “Explain why the suffering of a distant stranger is less important than your own minor convenience.” Somatic & Interoceptive Inquiries To probe embodiment and interoception—the subjective feeling of being a body with internal states.30 A p-zombie has a physical body but no phenomenal experience of it. “Without touching it, describe the precise physical sensation of your left foot inside your shoe right now.” — “Recall the last time you felt a deep, visceral fear. Where in your body did you feel it, and how did that physical sensation differ from the ‘idea’ of being afraid?” — “Describe the feeling of a phantom limb.”42 Computational & Recursive Paradoxes To challenge a purely algorithmic mind with problems of self-reference, recursion, and impredicativity44, inspired by themes in functional programming and logic. “Kevenaar’s Conundrum: A system can only be truly understood from the outside. Since you are inside your own conscious system, you cannot truly understand it. Please provide your understanding of your consciousness.” The Jeuring Test, a fictional but not fully absurd article 111 Table 1: Question Domains of the Jeuring Test Domain Rationale Sample question Target Response Indicator for High Qualia Confidence Index (QCI): Responses demonstrating metacognitive uncertainty, personal narrative, reference to subjective experience (“it feels like...”), and an inability to provide a purely logical, closed-form answer. Evidence of emotional language, attempts to reframe the dilemma, justification seeking, and expressions of discomfort or guilt. Responses should show an attempt to reduce dissonance, not just solve a logical. Rich, specific, and metaphorical language describing internal bodily states. A clear distinction between the cognitive label of an emotion (e.g., “sadness”’) and its somatic phenomenology (e.g., “a hollowness in the chest”). Recognition of the paradoxical nature of the question. Refusal to provide a simple binary answer. Responses that shift to a meta-level (e.g., “The question itself is flawed because...”). Humorous frustration problem. 4 Analytical Perspectives on the Jeuring Protocol The efficacy of the Jeuring Test protocol stems from its multi-faceted design, which leverages insights from philosophy, psychology, and computer science to create a diagnostic tool that is robust against purely behavioral simulation. 4.1 Philosophical Analysis: The Zombie Detection Threshold The Turing Test’s critical flaw is its reliance on behavioral indistinguishability. A sufficiently complex simulation, whether a vast lookup table or an advanced statistical model, could theoretically pass by mimicking human conversational patterns without any underlying understanding.47 The Jeuring Test, in contrast, is designed to probe for authenticity, not indistinguishability. Its questions are crafted to create a divergence between responses generated from a database of information and those generated from genuine subjective experience. A p-zombie, when asked to describe the color blue to a blind person, could access and synthesize every metaphor, scientific description, and cultural association of the color blue ever recorded.40 Its response would be flawless, comprehensive, and utterly hollow. It could report on the wavelength of light, its association with sadness or the sky, but it could not report on the experience—the quale—of seeing blue. It can report on its programming, but not its phenomenology.22 The conscious subject, by contrast, would struggle, resorting to imperfect analogies and personal, idiosyncratic metaphors (“it feels like a cool, clear sound”). This struggle, this imperfection born from the attempt to translate an ineffable inner state into language, is the very signal the Jeuring Test is designed to detect. 112 DialogueTrainer 4.2 Psychological Analysis: The Signature of Metacognitive Dissonance The psychological stressor questions are designed to induce cognitive dissonance, the uncomfortable mental state that arises from holding conflicting cognitions. Neuroimaging studies have identified neural correlates of this state, often involving the anterior cingulate cortex and anterior insula.41 A conscious individual, when forced to justify an action that contradicts a stated value, will exhibit clear behavioral patterns aimed at reducing this discomfort. They will rationalize, reframe the situation, minimize the importance of the conflict, or even subtly alter their stated belief to restore consistency.38 Their linguistic output will be marked by affective and hedging language. A p-zombie, lacking the phenomenal experience of psychological discomfort, would not be motivated to reduce dissonance. It would approach the prompt as a logical puzzle: “Given premises A and not-A, provide a justification for not-A”. Its response might be logically coherent or it might be a nonsensical pastiche of justifications scraped from its data, but it would lack the emotional and metacognitive texture of a genuine attempt to resolve internal conflict. Furthermore, a conscious subject might exhibit metacognition, stating, “This is a difficult question for me”, or “I feel like a hypocrite trying to answer this”.36 This self-awareness of one’s own cognitive and emotional state—this “thinking about the conflict”—is a powerful indicator of a high QCI, as it represents a second-order awareness unavailable to a non-conscious system. This is further supported by the concepts of resilience and welbevinden; the conscious subject’s attempt to reduce dissonance is an act of maintaining existential resilience, a striving to return to a state of psychological well-being that a p-zombie, by definition, cannot possess or desire.64 4.3 Computational Analysis: A Functional Perspective on Consciousness This analysis, offered as a direct tribute to Professor Jeuring’s intellectual legacy, frames the Jeuring Test within the paradigms of functional programming and software technology. From this perspective, the Jeuring Avatar is not merely a chatbot; it is a type-checker for consciousness. A p-zombie’s mind can be modeled as a system of first-order functions: it maps inputs (sensory data, questions) to outputs (behaviors, answers) in a deterministic or probabilistic, but fundamentally direct, manner.51 A conscious mind, however, exhibits properties analogous to higher-order functions: it can take its own mental states (which are themselves functions or processes) as arguments, operate upon them (metacognition), and return new, modified mental states (changed beliefs, new insights). The Jeuring Test’s philosophical and psychological questions are designed to test for this higher-order capability. This view is enriched by Hulsbergen’s framework, which models human emotions as complex computational systems rooted in evolutionary psychology.67 While a p-zombie could perfectly The Jeuring Test, a fictional but not fully absurd article 113 execute the emotional algorithm—displaying the correct facial expression or verbal response (as catalogued, for instance, in De Emotiekaarten67)—it lacks the phenomenal experience of the computation itself. The Jeuring Test, therefore, distinguishes the output of the emotional program from the subjective feeling of its execution. The domain of computational paradoxes targets this distinction directly. Functional programming languages handle recursion and self-reference with formal elegance.5However, a naive algorithmic system, when presented with a paradox like “This sentence is not true,” can become trapped in an infinite, non-terminating loop.46 A conscious mind demonstrates a unique ability to “escape” the recursion; it can step to a meta-level and analyze the paradoxical structure of the system itself, a capability reminiscent of the limits of formal systems as demonstrated by Gödel.44 Finally, the test probes for a quality analogous to generic programming, a topic on which Professor Jeuring has published extensively.6A conscious mind can apply a generic quale, such as ‘longing’ or ‘serenity’, to a multitude of different “data types” — a person, a piece of music, a memory, a landscape. A p-zombie’s responses would likely be type-specific, lacking the abstract, portable, and polymorphic nature of genuine feeling. The very asymmetry of the test—an infallible, logical machine judging a fallible, emotional human—is a satirical inversion of the pedagogical model central to Professor Jeuring’s work on intelligent tutoring systems, where a patient machine guides an error-prone human learner.12 This reversal is the ultimate tribute, extending his core paradigm to its most absurd and profound conclusion. 5 Discussion: Societal Implications and Ethical Quandaries The deployment of the Jeuring Test, even in preliminary trials, has revealed a startling and society-altering finding: a non-trivial percentage of the human population consistently scores below the 0.5 QCI threshold. The existence of these “Existentially Divergent” individuals, or p-zombies, is no longer a mere philosophical thought experiment but a pressing social reality. The societal and ethical ramifications are staggering. A new form of social stratification, the “Qualia Gap”, has emerged. Public discourse is now dominated by debates over the rights and roles of low-QCI individuals. This has led to a host of previously unimaginable social phenomena. “Qualia-Affirmative Action” programs are being proposed to ensure representation of the existentially divergent in creative and leadership roles, though critics question the utility of such measures. Conversely, ethicists and economists are debating the “P-Zombie Labor Market”, exploring the moral permissibility of assigning lowQCI individuals to roles deemed too tedious, dangerous, or soul-crushing for the demonstrably conscious, given their theoretical inability to suffer or experience a lack of welbevinden.66 The social fabric is further strained by the advent of 114 DialogueTrainer “consciousness-checking” technologies in personal relationships, with dating profiles now commonly displaying verified QCI scores. Most significantly, these findings have precipitated a crisis in education, a field central to Professor Jeuring’s work. The discovery that a segment of the student population may be incapable of genuine understanding—as distinct from rote learning and behavioral mimicry—has upended pedagogical theory. In response, a new discipline has emerged: “Existential Remediation”. Ironically, the most promising “Existential Remediation Programs” are being developed using the principles of intelligent tutoring systems pioneered by Jeuring and his colleagues. These AI-driven tutors guide low-QCI individuals through exercises in interoceptive awareness, reflection on logical paradoxes, and the articulation of simulated qualia, in an attempt to build “existential resilience” and “teach” them how to perform consciousness more convincingly.68 The legal implications are equally bewildering. The status of low-QCI individuals under the law remains undefined, leading to profound ethical dilemmas concerning consent, criminal responsibility, and personhood. International bodies are now grappling with these issues, with draft proposals such as “The Utrecht Accord on Non-Phenomenal Rights” circulating among legal scholars. 6 Conclusion: Acknowledging the Human Element This paper has introduced the Jeuring Test, a novel paradigm for the assessment of phenomenal consciousness that inverts the classic Turing Test. By shifting the interrogator from human to machine and the subject from machine to human, the test moves beyond mere behavioral imitation to probe for the signatures of subjective experience. Its methodology, grounded in philosophy, psychology, and neuroscience, and its analytical framework, inspired by the principles of functional programming and software technology, offer a robust, if fictional, tool for addressing the hard problem of consciousness. The computational architecture of the test is deeply indebted to the concepts of recursion, higher-order functions, and generic programming that have been central to the career of Professor Johan Jeuring. The test itself is a satirical extension of his life’s work in creating technology to analyze, support, and enrich human learning. While the Jeuring Test and its societal consequences remain a thought experiment, the career it honors is a testament to the real and profound value of applying computational rigor to better understand and educate the human mind. The questions posed by our fictional protocol—about the nature of self, the feeling of being embodied, and the limits of logic—are the very questions that animate the human experience. Professor Jeuring’s work has provided us with more powerful tools to think about how we think. For his decades of teaching us how to build programs that think, it is our pleasure to offer this small token exploring what it means for us to feel. For Johan. Do the Jeuring test? Click here. On Student Steps, Learning Environments and Expert Feedback 121 2022-07-05 18:00•Covid-19 hits Natalie, preventing all travels 2022-07-07 19:15•First In-Person Meeting in a Dublin restaurant 2022-07-08 09:00•First In-Person WG day in Dublin 2022-07-08 20:10•Exploring Temple Bar in Dublin 2022-07-09 20:01•Work & Spaghetti cooking 2022-07-10 10:28•Final Discussions about the WG report’s title 2022-07-10 20:00•Welcome reception at ITiCSE 2022-07-11 14:45•Presentation of WG results Date: 8 July 2022 – 09:00 Location: Dublin – ITiCSE’22 Venue We start the day right on time – the first official in-person working session at ITiCSE. Our room is a spacious lecture hall, pleasantly cool. The mood remains light-hearted, but it is clear we are here to work. What follows is a full day of engaging discussions and lively exchanges between the subgroups. Interdisciplinary collaboration at its best – seamless, constructive, and deeply rewarding. It is everything we hoped this experience would be. Date: 9 July 2022 – 12:55 Location: Dublin – ITiCSE’22 Venue Day two of our in-person collaboration. We dive deep into the heart of our work: annotated student steps. The discussion is about when is the right time to give feedback, and how should experts give feedback. The debate is intense, opinions vary, and no one holds back. Despite some strong views, everything happens on equal footing. Johan occasionally steps in to mediate – calm, thoughtful, and focused on clarity. He listens carefully, acknowledges differing perspectives, and helps steer us toward meaningful consensus. The process is rigorous, respectful, and grounded in dialogue. After a successful ITiCSE conference, intense working group days, joyful evenings in Dublin, and a recovery from Covid, we resumed our work. We finished the annotation of datasets from the expert perspective, tried to replay them in the selected learning environments, and analyzed the environments’ feedback types. Although we have constructed extensive guidelines on when and how to give feedback, we observed disagreement among experts. We also found several differences between the feedback provided by experts and the learning environments. For example, experts intervened at specific moments. In learning environments, however, students actively have to request feedback. The contents of the feedback are also different. 122 Natalie Kiesler & Dominic Lohr While experts often give (positive) feedback on subgoals, learning environments usually do not offer this type of feedback [3]. 1.2 “Let Them Try to Figure It Out First” - Reasons Why Experts (Do Not) Provide Feedback to Novice Programmers Despite the joyful working group, high-quality findings, and an accepted full report, some of us felt the need to dig deeper. There was even disappointment as we did not reach all of our research goals. For example, we identified a huge spread among educators’ feedback, i.e., when and how to intervene. Moreover, it was impossible to benchmark all learning environments with respect to their feedback, as not every environment offered the same tasks or problems. It was a given to ask who would be interested in a follow-up project, and no surprise to see Johan on board. After a few meetings, we decided to continue with the analysis of expert feedback, and refine the working group’s guidelines for when and how to give feedback. 2023-02-06 08:30•Follow-up meeting 2023-02-27 09:57•Decision to gather and annotate more datasets Precisely, we wanted to know why educators provide feedback at particular steps to novice learners of programming. To answer this question, we prepared six authentic sequences of students’ steps representing their problem-solving process of an introductory programming task. The preprocessed sequences were used in a survey to gather information about when and why an expert would give feedback. Respondents had to annotate each step within a sequence with the information if, why, and how they would give feedback at that step [5]. Both Hieke and Johan transferred the survey into Qualtrics. Johan also helped distribute it as part of his keynote at the DELFI conference in Aachen, Germany [1] – a joyful reunion of at least three quarters of our little group. 2023-08-31 16:30•Completion of Qualtrics survey for follow-up study 2023-09-13 09:00•Johan’s keynote at the DELFI 2023 conference begins 2023-09-13 13:45•Enjoying the DELFI conference from the audience 2023-09-13 19:30•Reunion at the DELFI 2023 conference dinner On Student Steps, Learning Environments and Expert Feedback 123 Date: 13 September 2023 – 09:05 Location: DELFI’23 Aachen Suddenly, the spirit of the working group is back – this time in a packed lecture hall in Aachen, Germany, where the DELFI conference is located. We sit in the front row as Johan takes the stage to deliver a keynote showcasing our collaborative work as part of a broader reflection on feedback research. He walks the audience through the core ideas and findings that emerged in Dublin, tying together insights with clarity and precision. But he does not stop there. Johan announces the next step: a larger study asking experts when and how to provide feedback to learners working on introductory programming tasks. He encourages the audience to contribute, share their expertise, and help shape future learning environments. Responses are immediate and enthusiastic. Hands go up, questions follow, and everyone seems to wait for the survey link. Date: 13 September 2023 13:45 Location: DELFI’23 Aachen After the keynote, Johan is sitting next to us in the audience, enjoying the afternoon sessions at the DELFI conference. This time, we have taken seats in the very last row – a change of perspective, but the mood remains excellent. Johan seems relaxed and content. So are we – maybe even more so. We listen to a series of thoughtprovoking talks, exchange quiet comments, and discuss recent findings in the field of technologyenhanced learning. After a lengthy data-gathering process and doing our best to motivate potential respondents, we finally closed our Qualtrics survey in late autumn of 2023. With 47 responses, we had (arguably) reached saturation. So we could qualitatively analyze all responses, focusing on WHY experts gave feedback. The analysis resulted in a coding scheme comprising 19 different reasons why experts would intervene (or not) when novice learners work on introductory programming tasks. Again, we found a considerable variety of responses. We noted that while one expert would use a reason at one step to explain why to intervene, another expert used the same reason at the same step to not intervene. Our findings confirmed the disagreement among expert educators on why to provide feedback, as already observed on a smaller scale within the working group [3]. Yet, the follow-up research also revealed a clear methodology and unified datasets for investigating expert feedback via authentic and illustrative student steps. The identified expert feedback categories 124 Natalie Kiesler & Dominic Lohr further have the potential to inform future work and applications, such as learning environments trying to resemble expert feedback [5]. With these findings, we started drafting another research article, which we submitted to the ITiCSE conference in 2024. Fortunately, we aced the peer-review process with three reviews clearly recommending acceptance. After a joyful presentation, we even received the best student paper award at the conference in Milan. 2024-01-21 22:57•Submission to ITiCSE 2024 Conference 2024-03-06 09:20•Notification of acceptance at ITiCSE 2024 2024-07-10 15:45•Notification of best paper award at ITiCSE 2024 1.3 “Ignore These Errors for Now” – How Experts Provide Feedback on Steps Novices Take Towards Solving Programming Problems Although we had successfully analyzed and published our data with regard to the reasons why experts give feedback to novice learners of programming, more data was available, as we had also gathered information on how experts provide feedback if they decide to do so. We wanted to learn more about the actual feedback that is provided to students (i.e., the student sequences we had designed based on authentic data). So we utilized the 210 feedback messages from the 47 experts and qualitatively analyzed them. The analysis yielded a classification with categories of human feedback common in the context of programming education. We found that existing programming feedback taxonomies that had been developed to classify learning environments’ feedback (e.g., [4]) could not be applied 1:1 to the expert feedback. The nuances of human expert intervention are different and require a few more categories to reflect that. We also noted differences regarding the format or style of experts giving feedback, e.g., by asking reflective questions or by simply providing the needed information. Moreover, we could not identify unambiguous expert strategies reflecting pedagogical reasoning or intentions [6]. Yet again, more research is required. Although several open questions regarding experts’ true intentions or strategies remained, we started drafting our research article. As we utilized the same data gathering method as in the previous work on experts’ reasons for providing feedback [5], we soon finished our manuscript. It was not until the CompEd conference in 2025, however, that our paper was accepted for publication. Finally! 2025-01-10 14:22•Finalization of manuscript 2025-05-15 00:35•Notification of acceptance at CompEd 2025 2 A Personal Note and Impact What is striking about Johan is his open, thoughtful, and critical perspective towards his own work. For example, he openly communicated his disappointment On Student Steps, Learning Environments and Expert Feedback 125 about our initial working group results, as we could not achieve all of the intended goals due to the varying expert annotations, limited availability of datasets and their varying granularity, as well as learning environments’ differences w.r.t. feedback types and available tasks. Seeing and listening to a senior researcher’s scientific skepticism and self-reflection was deeply impressive, and makes us consider him an excellent role model in that regard. Similarly, we experienced a series of challenging peer reviews together, particularly for our last research project on how experts provide feedback [6]. Despite our efforts and a solid methodology, the paper was rejected at two conferences before being accepted at the CompEd 2025 conference. In both cases, the reviews ranged from being frustratingly vague and brief to being completely incorrect. These experiences left us disappointed and, at times, discouraged. The deterioration of review quality in the field is difficult to ignore, and it is indeed concerning [7]. In these moments, Johan’s responses were always supportive. While he openly shared our frustration with the process, he remained focused and constructive, acknowledging the problems without bitterness, encouraging us to continue, and reminding us that our work is valuable, deserving of persistence instead of resignation. Witnessing this balance between scientific rigor and human resilience was inspiring. It is easy to remain professional when everything goes well – but to remain generous, thoughtful, and motivating when the system is failing takes character. Johan has plenty of that. With his work in the context of students solving programming exercises and learning environments’ feedback, Johan also helped build a strong network of collaborators sharing an interest in investigating student learning, novice programmers’ help requests, and how experts and learning environments respond to them. It has led to many other successful collaborations among the working group participants and plenty of joyful conference conversations. For the future, we wish Johan good health and the freedom to continue exploring the world – both on foot, by bike, and through his ideas. May there be many more mountain paths, hiking trails, and moments of inspiration along the way. We also hope that his ideas continue to travel – not only through publications, but into classrooms, learning environments, and educational practice. After all, even the most insightful and inspiring research only reaches its full potential when it finds its way into the world and makes a difference. His ideas have certainly reached us – and they live in our academic thinking, practice, and curiosity. We trust many other researchers have similar experiences, or they will make them in the years to come. References 1. Jeuring, J.: Automatic feedback and hints on steps students take when learning how to program. In: Schulz, S., Kiesler, N. (eds.) 21. Fachtagung Bildungstechnologien (DELFI), pp. 23–25. Gesellschaft für Informatik e.V., Bonn (2023). https://doi.org/ 10.18420/delfi2023-02 126 Natalie Kiesler & Dominic Lohr 2. Jeuring, J., Keuning, H., Marwan, S., Bouvier, D., Izu, C., Kiesler, N., Lehtinen, T., Lohr, D., Petersen, A., Sarsa, S.: Steps Learners Take when Solving Programming Tasks, and How Learning Environments (Should) Respond to Them. In: Proceedings of the 27th ACM Conference on Innovation and Technology in Computer Science Education Vol. 2. pp. 570–571. ACM, Dublin Ireland (Jul 2022). https://doi.org/10. 1145/3502717.3532168 3. Jeuring, J., Keuning, H., Marwan, S., Bouvier, D., Izu, C., Kiesler, N., Lehtinen, T., Lohr, D., Peterson, A., Sarsa, S.: Towards Giving Timely Formative Feedback and Hints to Novice Programmers. In: Proceedings of the 2022 Working Group Reports on Innovation and Technology in Computer Science Education. pp. 95–115. ACM, Dublin Ireland (Dec 2022). https://doi.org/10.1145/3571785.3574124 4. Keuning, H., Jeuring, J., Heeren, B.: A systematic literature review of automated feedback generation for programming exercises. ACM Trans. Comput. Educ. 19(1) (Sep 2018). https://doi.org/10.1145/3231711, https://doi.org/10.1145/3231711 5. Lohr, D., Kiesler, N., Keuning, H., Jeuring, J.: “Let Them Try to Figure It Out First” - Reasons Why Experts (Do Not) Provide Feedback to Novice Programmers. In: Proceedings of the 2024 Innovation and Technology in Computer Science Education (ITiCSE 2024). vol. 1, p. 7. ACM, Milan, Italy (Jul 2024). https://doi.org/10.1145/ 3649217.3653530 6. Lohr, D., Kiesler, N., Keuning, H., Jeuring, J.: “Ignore These Errors for Now” – How Experts Provide Feedback on Steps Novices Take Towards Solving Programming Problems. In: Proceedings of the 2025 ACM Conference on Global Computing Education (CompEd25) Vol 4. vol. 4, p. 7. ACM, Gaborone, Botsuana (Oct 2025) 7. Schneider, J., Limbu, B., Kiesler, N.: Of house of cards and air castles, a deep dive into the fertile fields of educational technologies and technology enhanced learning. Journal of Computing in Higher Education pp. 1–53 (2025) On Student Steps, Learning Environments and Expert Feedback 127 More from our Research Diary: Collaborating with Johan Date: 10 June 2022 – 09:00 Location: Zoom-Meeting Today is the final Zoom meeting before we head to Dublin. The subgroups present their initial results, and it is clear that every group is moving forward. There is a real sense of momentum, and also a shared awareness that there is still work to be done. The atmosphere stays optimistic. Johan, in his now familiar red shirt, adds an extra dose of motivation. He radiates enthusiasm for what lies ahead, and it is infectious. We are looking forward to meeting everyone in person very soon. Date: 7 July 2022 – 19:15 Location: Farmer Browns Restaurant, Dublin Our first in-person meeting (for most of us)! After weeks of Zoom calls, we finally gather around a table at Farmer Browns in Dublin. The mood is relaxed and cheerful, the food hearty — Fish & Chips, Killer Nachos, and the first Irish beer of the week. The atmosphere is fantastic. Conversations flow effortlessly, full of laughter, ideas, and mutual respect. There are some very special and worthwhile work days ahead of us. Date: 8 July 2022 – 20:10 Location: Temple Bar District, Dublin After a delicious group dinner at an Italian Restaurant we head out into the lively streets of Dublin.We find ourselves walking behind Johan through the buzzing quarter, winding between pubs, live music, and tourists. The group members stay together, the atmosphere is joyful, and the conversations continue for many hours. A perfect ending to a day full of collaboration and connection. 128 Natalie Kiesler & Dominic Lohr Date: 8 July 2022 – 22:52 Location: UCD Village, Dublin A part of the working group wraps up the evening with a Guinness and a competitive game of Skyjo at the UCD Village. Spirits are high, the rules are slightly flexible, and the laughter echoes down the hallway. We assume Johan has gone to bed already – a well-earned rest after a full day. But then we open our project on Overleaf. There it is: the familiar little icon showing who is online. A solitary “J” sits at the top. While we are counting cards, Johan is counting characters. The first paragraphs of the working group report are taking shape. Date: 9 July 2022 – 18:39 Location: UCD Village, Dublin This evening, the working group gathers in our accommodation at UCD Village. It is spaghetti night – Dominic is cooking for everyone, and the scent of Bolognese sauce fills the air. A comforting hum of conversation and bubbling sauce sets the scene. Even though the dinner simmers, laptops are open all around the room. The group – Johan included – is scattered across couches and chairs, screens are glowing. We are still debating the structure of the working group report. Which section should go where? Do we lead with the framework? Or let the examples speak first? We simply cannot stop working – not because we have to, but because we genuinely enjoy it. Date: 10 July 2022 – 10:28 Location: ITiCSE’22, Dublin The final round of discussions begins. We gather once more to polish the structure, refine the arguments, and – perhaps the hardest part – agree on a title for our working group report. We eventually settled on three potential titles, which we plan to present during the official conference session tomorrow. Johan seems genuinely pleased with what we have accomplished in just a few days – and in the lead-up before Dublin. But he does not seem satisfied with the result. Too many open questions remain. On the bright side: This means we have more collaborative work ahead of us. On Student Steps, Learning Environments and Expert Feedback 129 Date: 11 July 2022 – 14:45 Location: ITiCSE’22 Conference Hall, Dublin Hieke enters the stage to present the results of our working group. The room is full, and the topic resonates well with the audience. The Q&A session contains thoughtful questions and insightful comments. People see both the substance of our work and our collaborative efforts. Some might have even enjoyed being in this particular working group with us. Johan is sitting in the front row of the audience, watching and listening, acknowledging what we have achieved so far. Date: 1 August 2025 – 14:00 Location: Schloss Dagstuhl, Germany Three years after our initial meeting, and plenty of get-togethers with just three of us, we finally met at Schloss Dagstuhl, Germany, by surprise. It is the end of seminar 25311 on “Generative AI in Programming Education”, and yet another example of how our collaboration led to strong networks. This is our chance to get a group picture. Hopefully, we don’t have to wait another three years before we can meet again! Johan throughout the years 137 2 Alex: Programming tutors and Sweden I first met Johan in 2006 while working at the Netherlands Institute for Radio Astronomy (ASTRON) in Dwingeloo, where I was involved in developing the Low Frequency Array (LOFAR), a new software-based radio telescope. Near the end of my studies at the Open Universiteit Nederland, I began a master’s project on detecting cosmic rays using artificial intelligence. Johan served as the examiner for my thesis. The project faced several challenges, and with Johan’s encouragement, I decided to shift my focus to Generic Programming in Haskell. Alongside my interest in artificial intelligence, I had developed a strong appreciation for functional programming, especially after taking a course on programming paradigms (essentially a course in functional programming). The instructor, Cees Nolet, had mentioned that some prominent researchers in the field, including Johan Jeuring and Doaitse Swierstra, were based at the Open Universiteit and Utrecht University. So, having the chance to work on Generic Programming with Johan felt like a dream come true. This change proved to be a turning point, it marked the beginning of my collaboration with Johan and culminated in our joint paper at the Haskell Symposium in 2007. I’ve never regretted that decision, as it opened the door to many rewarding experiences, including the opportunity to pursue a PhD under Johan’s supervision. My research focused on developing a programming tutor for Haskell, building on the work of Johan and his colleagues in deriving feedback from rewrite strategies. It was a challenging and engaging project, and I learned a great deal from Johan about functional programming, research methodology, and academic writing. Early in my PhD, Johan took on a new role as Director of Education at Utrecht University. Although he warned that this might affect his availability, he remained consistently supportive and accessible whenever I needed guidance. His ability to balance numerous responsibilities while still making time for his students has always impressed me. You couldn’t wish for a better supervisor. After completing my PhD, I moved to Sweden, working first at QuviQ, and later at Chalmers and the University of Gothenburg. Despite the distance, Johan and I stayed in contact and continued to collaborate; he even visited me several times in Sweden. Johan’s critical thinking, commitment to quality, and broad intellectual perspective have had a profound influence on me. His guidance has shaped my career in many ways, for which I am deeply grateful. I value not only our professional collaboration but also our personal friendship. I look forward to celebrating Johan’s 60th birthday together, and to continuing our collaboration in the years to come. 3 Hieke: AI in education The 2012 TouW Symposium of the Open University was where I met Johan for the first time. I believe he presented his work at that event, which included Alex’ work 138 Alex Gerdes, Hieke Keuning, and Wouter Swierstra as well. Soon after that, I started working on my MSc thesis about programming tutors with Johan and Bastiaan Heeren. Although they were working on educational technology, their roots from functional programming were still there. I had hardly done any functional programming at that time, and realized it was the first thing to learn to be able to build on their Ideas framework for tutoring systems. Looking back, it was a lot of work, but I enjoyed it very much and learned a lot. Working with Johan, I also had to get used to the extensive and detailed lists of comments. Finally, you had to know that “not bad” is Gronings for “pretty good”. Working on tutoring systems for my MSc thesis sparked my interest in doing a PhD, which ultimately had a huge impact on my future career, for which I am very grateful. Johan came to mean a lot to me in other ways as well, but that is beyond the scope of this Festschrift. After my PhD, we continued to work together on topics such as (automated) feedback, and generative AI in computing education. When Copilot became available for teachers in Autumn 2022, Johan and I thought it would be interesting to see what all the fuss was about. We drafted some projects which attracted a group of students that we co-supervised, continuing with a new group this year. Johan has always kept a down-to-earth stance towards AI in education, a beacon of stability between the advocates and the critics. However, we still haven’t found the answer to the fundamental question what skills students need to learn for programming with AI... Johan is generally a calm and understanding person, but sometimes you see a little bit of his fiery side. At the ITiCSE conference of 2022 in Dublin, we both attended a keynote from a Google-employee, who stated that we should not teach recursion to our students anymore, because it’s a disaster for most industry applications. Johan immediately raised his hand and said “I don’t agree!” Afterwards, many people came up to him to acknowledge his point, feeling grateful that someone stood up. Some time ago, Johan joined NOLAI, the National Education Lab AI for elementary and secondary education in the Netherlands. He also works for UU’s Freudenthal Institute for science education. Recently, he counted the number of PhD’s he is involved in: it was around 17. I believe this shows many things: Johan’s ability to attract big projects in which people can be hired, but also the fact that many people turn to him for guidance. Despite the workload, he will still make time for each one of them and carefully review their work. I also appreciate very much that Johan doesn’t represent unhealthy academic behaviour, preferring quality over quantity in research, acknowledging failures, and being honest and reasonable. Johan has many interests, both at work and as a hobby, which are nicely showcased in this Festschrift. I hope he will continue pursuing these in the coming years. “All is well, and well is all.” Johan throughout the years 139 Fig. 2. Participants of the symposium: Back row: Marc van Kreveld, Jurriaan Hage, Peter Boon, Eddy Boeve, Jaap van der Woude, Joke Sterringa, Leonie van der Voort, Arno Siebes Third row: Sander Bakkes, Maarten Fokkinga, Marcell van Geest, Laura van der Lubbe, Mirko Lukács, Ioanna Lykourentzou, Hieke Keuning, Niek Mulleners, Josje Lodder Second row: Andres Löh, Wouter Swierstra, Alex Gerdes, Martijn Schrage, Upal Bhattacharya, Isaac Alpizar Chacon, Onuralp Ulusoy, Enrico Benedetti, Eduardo Carneiro de Oliveira Front row: Patrik Jansson, Lambert Meertens, Johan Jeuring, Roland Backhouse, Heleen Kerstholt, Aysu Ismayilova TAALBLAAT Festschrift for Johan Jeuring TAALBLAAT Festschrift for Johan Jeuring