Bicara matematika: Teorema tentang sistem kontrol revisi git?

Saya ingin memberikan ceramah matematika tentang sistem kontrol revisi git . Sekarang ini banyak digunakan dalam matematika serta industri ilmu komputer. Sebagai contoh, komunitas HoTT (Homotopy Type Theory) menggunakannya, dan itu adalah sistem go to untuk pengeditan kolaboratif dari file teks, apakah itu kode sumber atau marka lateks.

Saya tahu git menggunakan gagasan grafik asiklik terarah, yang merupakan permulaan. Namun, ceramah matematika yang baik menyebutkan bukti dan teorema.

Teorema apa yang mungkin saya buktikan tentang git yang sebenarnya relevan untuk digunakan?

Sebuah repositori git dapat dianggap sebagai seperangkat revisi yang dipesan sebagian (di mana satu revisi lebih awal dari yang lain dalam urutan jika itu adalah penerus langsung atau tidak langsung dari yang sebelumnya). Pesanan parsial yang Anda dapatkan dari repositori git cenderung memiliki lebar rendah (ukuran kumpulan terbesar dari revisi yang saling independen) karena lebar terkait langsung dengan jumlah pengembang aktif dan jumlah garpu berbeda yang mungkin dikembangkan oleh masing-masing pengembang. di.

Berdasarkan latar belakang ini, saya akan menyarankan teorema Dilworth , yang menyatakan bahwa lebar urutan parsial sama dengan jumlah minimum rantai (himpunan bagian yang dipesan secara total) yang diperlukan untuk mencakup semua versi. Dan untuk membuatnya sesuai topik untuk forum ini, Anda juga bisa menyebutkan algoritma berbasis pencocokan grafik untuk menghitung lebar dan menemukan penutup dengan jumlah minimum rantai dalam waktu polinomial.

Salah satu cara ini mungkin relevan untuk penggunaan aktual di Git adalah dalam sistem untuk memvisualisasikan riwayat versi suatu sistem: sebagian besar sistem visualisasi Git yang saya lihat menarik waktu pada sumbu vertikal, dan versi independen dari repositori secara horizontal, jadi ini akan memberi Anda cara untuk mengatur visualisasi menjadi sejumlah kecil trek vertikal independen.

Atau, jika Anda menginginkan sesuatu yang lebih ambisius dan maju, coba struktur data pohon menyalahkan Demaine et al. , Yang secara langsung dimotivasi oleh resolusi konflik dalam sistem kontrol versi yang mirip git.

Menariknya, ada matematika yang baru lahir dari sistem kontrol versi, meskipun pada titik ini hanya berlaku sebagian untuk Git. Ini disebut teori tambalan [1, 2, 3, 4, 5] dan muncul dalam konteks sistem kontrol versi DARCS. Ini bisa dilihat sebagai teori abstrak tentang percabangan dan penggabungan . Baru-baru ini teori patch telah diberikan perawatan HoTT [6] dan kategoris [7].

Teori patch sedang dalam proses, dan tidak mencakup semua aspek kontrol versi, tetapi berisi banyak teorema yang bisa Anda lihat. Ini adalah contoh yang jelas dari teori yang berlaku untuk 'dunia nyata' - tidak mengherankan, karena teori patch adalah abstraksi / penyederhanaan dari sesuatu yang sangat konkret. Pada saat yang sama terhubung dengan matematika mutakhir seperti HoTT.

1. J. Dagit, Perubahan Tipe-Benar - Suatu Pendekatan Aman untuk Implementasi Kontrol Versi .
2. G. Sittampalam, Beberapa properti teori patch darcs .
3. I. Lynagh, Teori Jalur Camp.
4. D. Roundy, Menerapkan formalisme tempelan patch ... dan memverifikasinya.
5. J. Jacobson, A Formalisasi Teori Patch Darcs Menggunakan Semigroup Terbalik .
6. C. Angiuli, E. Morehouse, DR Licata, R. Harper, Teori Patch Homotopical .
7. S. Mimram, C. Di Giusto, Teori Kategorikal Patch .

Alternatif lain adalah melihat struktur data yang persisten (atau berfungsi murni). Struktur data internal Git dapat dilihat sebagai pohon persisten yang terus-menerus :

struktur data persisten adalah struktur data yang selalu mempertahankan versi sebelumnya dari dirinya sendiri ketika dimodifikasi. Struktur data seperti itu tidak dapat diubah secara efektif, karena operasinya tidak (secara kasat mata) memperbarui struktur di tempat, tetapi sebaliknya selalu menghasilkan struktur baru yang diperbarui.

Struktur data sebagian gigih jika semua versi dapat diakses tetapi hanya versi terbaru yang dapat dimodifikasi. Struktur data sepenuhnya persisten jika setiap versi dapat diakses dan dimodifikasi. Jika ada juga operasi berbaur atau menggabungkan yang dapat membuat versi baru dari dua versi sebelumnya, struktur data disebut terus-menerus persisten.

Ini pertanyaan yang relevan juga.

Ya, Anda secara matematis dapat menentukan cara kerja Git. Anda dapat mendefinisikan struktur Git primitif dan operasi Git pada mereka dan kemudian memiliki teorema yang membuktikan bahwa menggunakan operasi ini dengan cara tertentu mencapai tujuan tingkat lebih tinggi tertentu, atau upaya untuk mengkarakterisasi atau mengukur situasi di mana ini bukan masalahnya. (Misalnya, ketergantungan Git pada hash meninggalkan margin kecil untuk kesalahan.)

Gagasan lain adalah melakukan hal yang sama untuk Subversion, kemudian menghasilkan teorema yang membandingkan keduanya. Misalnya, sering dikatakan bahwa Git lebih baik dalam menangani penggabungan; Anda dapat memiliki teorema yang membuktikan ini, secara kualitatif atau kuantitatif.

Kegunaan akan sangat tergantung pada pembuatan abstraksi yang tepat. Menggambarkan secara matematis cara kerja kode sumber Git dalam semua detail tidak ada gunanya: kode sumber itu sendiri melakukan itu jauh lebih efektif dan ringkas.