Sprawdzacz dowodów w teori Typów Per Martin-Löf 'a
|
6 years ago | |
---|---|---|
project | 6 years ago | |
src | 6 years ago | |
.gitignore | 6 years ago | |
Eckmann-Hilton.prmk | 6 years ago | |
Nat.prmk | 6 years ago | |
README.md | 6 years ago | |
build.sbt | 6 years ago | |
compile.sh | 6 years ago | |
eh.prmk | 6 years ago | |
example.prmk | 6 years ago |
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)
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
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