Przemek-K0

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ń?)