Joukko-opin kaavojen automaattinen tarkastaminen MathCheck-ohjelmalla

Abstract

MathCheck on matematiikan opiskelemista tukeva ohjelma, joka tarjoaa opiskelijalle palautetta hänen työskentelystään. Syksyllä 2021 se tukee erityisesti reaaliaritmetiikan relaatioketjujen ja lineaarisen reaaliaritmetiikan päättelyketjujen tarkastamista. Tässä tutkielmassa otetaan askeleita kohti MathCheckin toiminnallisuuksien laajentamista joukko-opin kaavojen automaattiseen tarkastamiseen.

Joukko-oppimoodin käytännöllisen suunnittelun ja toteuttamisen pohjaksi kehitetään kirjallisuuden perusteella teoriaa matemaattisten joukkojen esittämisestä äärellisten automaattien avulla. Äärelliset automaatit ovat tietojenkäsittelytieteen ja matemaattisen logiikan rakenne, jotka kykenevät ilmaisemaan säännöllisiä kieliä. Kokonaislukujen lineaarisen aritmetiikan, eli Presburger-aritmetiikan kielellä esitettävät kokonaislukuvektorien joukot on mahdollista koodata säännöllisiksi kieliksi, ja siten myös esittää äärellisin automaatein. Näin saadaan tietorakenne, jolla on mahdollista kuvata myös äärettömiä joukkoja. Tämän teoreettisen pohdinnan tueksi ja ohjenuoraksi luodaan myös katsaus tarkastamisen, palautteen antamisen ja joukko-opin pedagogiikkaan MathCheckin näkökulmasta.

Tutkielmassa paitsi todistetaan uudelleen, että Presburger-joukkoja voidaan esittää äärellisin automaatein, myös täydennetään aihetta koskevasta kirjallisuudesta puuttuvia käytännön toteutukseen liittyviä yksityiskohtia. Näiden perusteella saadaan alustava kuva siitä, minkälaisia seikkoja käytännön toteutuksessa on tarkasteltava. Joukko-oppimoodin perusjoukoiksi kaavailtujen merkkijonojen säännöllisten kielten ja kokonaislukuvektoreiden Presburger-joukkojen kuvauksen lisäksi määritellään niiden avulla saatavan joukko-opin lauselogiikan ilmaukset, sekä pohditaan, minkälaisia MathCheck-tehtävänantoja tai -harjoittelutilanteita niiden avulla voisi muodostaa.

MathCheck is a program designed to support mathematics studies by providing a student with feedback on their work. In the autumn of 2021 it especially supports automated evaluation and checking of relation chains in real arithmetic and reasoning chains in linear real arithmetic. This study takes steps towards expanding the functionalities of MathCheck to automated checking of set theory formulas.

As the foundations for more practical planning and implementation of a set theory mode, a theory of representing mathematical sets using finite automata is developed. Finite automata are a structure in computer science and mathematical logic capable of expressing regular languages. Sets of integer vectors expressible in linear integer arithmetic, or Presburger aritmetic, can be encoded as regular languages, and therefore represented by finite automata. This provides a data structure that can contain even infinite sets. To support and guide this theoretical development, some attention is also paid to the pedagogy of checking, providing feedback and set theory from the point of view of MathCheck.

Apart from proving again that Presburger sets are representable by finite automata, this study also fills in some details pertaining to the practical implementation that are not given explicitly in the literature. They give a rudimentary understanding of the matters that a practical implementation must take into account. In addition to the regular languages consisting of strings and the Presburger sets consisting of integer vectors designed as the basic units of the set theory mode, a definition of the propositions expressible in a set theory derived from them is given, along with consideration of MathCheck exercises or practice situations available.