Sprawdzacz dowodów w teori Typów Per Martin-Löf 'a

Wojciech Karpiel 88a9b591d4 chyba działa troche O.o 5 years ago
project fc4256ce8a Spowrotem 2.12 5 years ago
src 88a9b591d4 chyba działa troche O.o 5 years ago
.gitignore 2f5c5ac68c +gitign 5 years ago
Eckmann-Hilton.prmk 88a9b591d4 chyba działa troche O.o 5 years ago
Nat.prmk 5d6e4834b6 bajery++ 5 years ago
README.md 7249ce6412 info o porzuceniu Scala Native 5 years ago
build.sbt fc4256ce8a Spowrotem 2.12 5 years ago
compile.sh ec79c70037 ID było niesamowicie popsute 5 years ago
eh.prmk 88a9b591d4 chyba działa troche O.o 5 years ago
example.prmk 5d6e4834b6 bajery++ 5 years ago

README.md

PRZEMEK

Sprawdzacz dowodów matematycznych implementujący teorię typów Per Martin-Löf'a https://en.wikipedia.org/wiki/Intuitionistic_type_theory

> $ sbt run 
Dzień dobry
Aktualnie zajmuje się sprawdzaniem typów.
Podaj coś to ci powiem jaki ma typ
np. polimorficza funkcja identycznościowa
(lambda (A (Universe 0)) (lambda (x A) x))
albo użyta do tyou jednostkowego
((lambda (A (Universe 0)) (lambda (x A) x)) Unit)
a potem zaaplikowana do przedstawiciela typu jednostkowego
(((lambda (A (Universe 0)) (lambda (x A) x)) Unit) tt)
Fajne co nie?
Inna opcja to wczytanie pliku z kodem
-f example.prmk

> $ sbt 'run -f example.prmk'
Kod: ((lambda (A (universe 0)) (lambda (x A) x)) unit)
Przed Bruinizacją: PiElim(PiValue(NamedType(A,Universe(0)),PiValue(NamedType(x,Var(A)),Var(x))),UnitType)
Ads: PiElim(PiValue(Universe(0),PiValue(Bruijn(0),Bruijn(0))),UnitType)
Znormalizowane: PiValue(UnitType,Bruijn(0))
Typ: PiType(UnitType,UnitType)

Zajawka

W pliku Nat.prmk można zobaczyć jak wygląda definicja liczb naturalnych, zera, następnika i mnożenia przez 2 gdy są zakodowane jako W-typ

Kompilacja

sbt package

Można odwrócić zmianę fc4256ce8a633254ea35b794ef41f2c07173d80f i kompilować rodzimo (przez Scala Native; porzuciłem to bo kod wynikowy jest wolny)

sbt 'set nativeMode := "release"' compile nativeLink
target/scala-2.11/przemek-out -f example.prmk 

Do zrobienia

  • wszechświaty
  • Pi-typy
  • Typy identycznościowe
  • Sigma-typy
  • Sumowane typy
  • W-typy
  • nazwane zmienne (żeby nie trzeba było DeBruijnami)
  • Deklarowanie stałych
  • strukturalna rekurencja
  • ogarnięte błędy kompilacji
  • ładne wypisywanie wyników
  • biblioteka twierdzeń (Eckmann-Hilton na początek)
  • Polimorficzność wszechświatów
  • Naprawienie błędów powstałych przy tworzeniu powyższego
  • Makra lispowe xD
  • Optymalizacja (pamięć znormalizowanych/sprawdzonych wyrażeń?)