dannypsnl / k Goto Github PK
View Code? Open in Web Editor NEWk theorem prover
Home Page: https://pkgs.racket-lang.org/package/k
License: Apache License 2.0
k theorem prover
Home Page: https://pkgs.racket-lang.org/package/k
License: Apache License 2.0
Example from Agda
open import Agda.Builtin.Equality
open import Data.Nat
data Fin : ℕ → Set where
fzero : ∀ {n} → Fin (suc n)
fsuc : ∀ {n} → Fin n → Fin (suc n)
_ : Fin 2
_ = fsuc fzero
_ : Fin 2
_ = fzero
Translated to k
(require k/data/nat)
(data (Fin [n : Nat]) : Type
[fzero : (Fin (s n))]
[fsuc (x : (Fin n)) : (Fin (s n))])
(check (Fin (s (s z)))
fzero)
(check (Fin (s (s z)))
(fsuc fzero))
#lang k
(require k/data/nat
k/data/bool)
(def (Nat-or-Bool [x : Bool]) : Type
[true => Nat]
[false => Bool])
(def a : (Nat-or-Bool true) z)
(def b : (Nat-or-Bool false) true)
The above program shows a simple type depends on the term sample, but it will get:
example/test2.rkt:10:28: type-mismatch: expect: `(Nat-or-Bool true)`, get: `Nat`
The following program shows problem:
(data (≡ [a : A] [b : A]) : Type
[refl : (≡ a a)])
(check (≡ z z)
(refl))
(check (≡ z (s z))
(refl))
Our unification didn't figure out this program has type mismatching.
We can use https://github.com/racket-tw/cover-badge to show test coverage of k.
(define-syntax-parser →
[(_ A B) #'(Pi ([_ : A]) B)])
I guess also rename it out as ->
For now, we have to write
(provide Nat s z)
We want
(provide (data-out Nat))
The only difference is their syntax-property
so I think they are mergeable.
test.rkt example is not working. Maybe related to #8
; /Users/ar/work/k/example/test.rkt:6:31: x: unbound identifier
; in: x
; Context (plain; to see better errortrace context, re-run with C-u prefix):
; /Users/ar/work/k/core.rkt:58:0 check-type
; .../parse/define.rkt:20:4
; /Users/ar/.emacs.d/elpa/racket-mode-20210727.1545/racket/syntax.rkt:66:0
Do you have more documentation about the package?
The interesting part is our CI do not crash
When type checking, unified universe level, and ensure it's a total order. We can build a directed graph that preserves <=
relationship by direction, then a graph without any rings is a valid type-construction.
To ensure our type checker works well with ill-form, we need a test set for cases that shall fail.
#36 constructs an example for it.
(def (fib [n : Nat]) : Nat
[z => z]
[(s z) => (s z)]
[(s (s n)) => (+ (fib (s n))
(fib n))])
The problem came from https://github.com/racket-tw/k/blob/develop/k-core/k/def.rkt#L91-L99; where should bind locals
recursively.
(data Bad : Type
[bad [x : (-> Bad X)] : Bad])
avoid bad type, ref to https://github.com/dannypsnl/plt-research/tree/develop/strictly-positive for implementation.
ref to agda: https://agda.readthedocs.io/en/v2.5.2/language/data-types.html#strict-positivity
ref: https://github.com/racket-tw/k/blob/develop/k-lib/k/data/nat.rkt#L21-L25
(def (Nat=? [n m : Nat]) : Bool
[z z => true]
[z (s m) => false]
[(s n) z => false]
[(s n) (s m) => (Nat=? n m)])
Error message:
dict-ref: no value found for key
key: #<syntax:k-lib/k/data/nat.rkt:25:19 Nat=?>
all keys: '(#<syntax:k-lib/k/data/nat.rkt:25:6 n> #<syntax:k-lib/k/data/nat.rkt:25:12 m>)
context...:
/Users/dannypsnl/racket.tw/k/k-core/k/core.rkt:73:0: typeof
/Users/dannypsnl/racket.tw/k/k-core/k/core.rkt:56:0: check-type
/Applications/Racket v8.4/collects/syntax/parse/private/parse.rkt:1020:13: dots-loop
/Applications/Racket v8.4/collects/syntax/wrap-modbeg.rkt:46:4
Currently, the following code cannot work
(def (identity [a : A]) : A
[a => a])
For example:
(def identity : (-> A A)
[m => m])
Need more description for our forms and libraries:
data
def
check
typeof
k/data/nat
k/data/bool
k/data/list
k/data/vec
k/equality
(def (symm {A : Type}
[x y : A]
[p : (≡ x y)])
: (≡ A y x)
[A x y refl => refl])
When we have different length of definitions (e.g. (≡ x y)
vs (≡ A y x)
), we'll get following errors:
→ racket k-lib/k/equality.rkt
andmap: all lists must have same size
first list length: 4
other list length: 3
procedure: #<procedure:unify?>
context...:
/Applications/Racket v8.3/collects/racket/private/map.rkt:275:2: gen-andmap
/Users/cybai/codespace/racket/k/k-core/k/core.rkt:57:0: check-type
/Applications/Racket v8.3/collects/syntax/parse/private/parse.rkt:1020:13: dots-loop
/Applications/Racket v8.3/collects/syntax/wrap-modbeg.rkt:46:4
however, we should be able to generate the type automatically to do pattern matching.
with a proper implementation, we should be able to see (≡ x y)
and (≡ A x y)
as same thing in the symm
function.
Cubical/HoTT variant language, e.g. #lang k/ube
left
, right
idp
?(def (refl {A : Type}
{a : A})
; `(≡ x y)` is short for `(Path _ x y)`, `Path` is equality in cubical
: (≡ a a)
[{A} {a} => (lambda (i) a)])
; invert is symmetric in cubical
(def (invert [A : Type]
[a b : A]
[p : (≡ a b)])
: (≡ b a)
; The path lambda contains current interval `i`
; to prove reverse result
; we invert the current interval `i` by using `~`
[A a b => (lambda (i) (p (~ i)))])
For example, https://github.com/wilbowma/cur/blob/main/cur/info.rkt. I suppose we will get a layout like
k/info.rkt
k-core/info.rkt
k-lib/info.rkt
k-test/info.rkt
k-doc/info.rkt
k-example/info.rkt
We have to ensure a definition is covering(no paths get ignored).
We can have different data type https://arxiv.org/pdf/2103.15408.pdf by @ice1000
A challenge will be how to encode the following behavior.
This pattern matching is not traditional pattern matching, say, it does not need
to be covering (although in the Vec example it is) and it can contain seemingly un-
reachable patterns (like duplicated patterns).
For example, Fin
type:
(data (Fin [n : Nat]) : Type
[(s n) => fzero]
[(s n) => (fsuc [x : (Fin n)])])
There might also have covering type, for example, Vec
type:
(data (Vec [A : Type] [N : Nat]) : Type
[A z => nil]
[A (s n) => (:: [a : A] [v : (Vec A n)])])
The link is how to match brace
And this is required for ≡
type:
(data (≡ {A : Type} [a b : A]) : Type
[refl : (≡ a a)])
(≡ A b c) ; good, apply implicit
(≡ b c) ; good
; same in pattern, full is all implicit
The idea is helping constructor expanded as it's name when no parameters, then no transformation would make pattern reference to constructor syntax, then syntax-property
should be accessible.
(check (≡ (+ (s z) (s z)) (s (s z)))
(refl))
; error
; cannot-unified: (+ (s z) (s z)) with (s (s z))
The above program cannot work properly, because our naive unification algorithm unifies (+ (s z) (s z))
with (s (s z))
directly. To fix this, we have to check if a term is not normalized, we shall normalize it.
To now, we still using a simulated pi type(of course make it weaker) that cannot be spread properly. I think now it's a good time to make it correct since it's all things' foundation.
Since now strict positivity check hasn't been enabled, the following program should be type-checked, but not(sadly).
(define-syntax-parser →
[(_ A B) #'(Pi ([x : A]) B)])
(data Bad : Type
[bad [f : (→ ⊥ Bad)] : Bad])
(def (self-app [b : Bad]) : ⊥
[(bad f) (f (bad f))])
(def (absurd) : ⊥
(self-app (bad self-app)))
Error message:
racket.tw/k/k-core/k/core.rkt:77:10: dict-ref: no value found for key
key: #<syntax:3-unsaved-editor:11:12 f>
all keys: '(#<syntax:3-unsaved-editor:10:6 self-app>)
related #3
(check (≡ (* (s z) (s z))
(s (s (s (s (s z))))))
(refl))
(data (List [A : Type]) : Type
[nil : (List A)]
[:: (a : A) : (List A)])
(data (Vec [E : Type] [LEN : Nat]) : Type
[vnil : (Vec E z)]
[v:: (e : E) (Vec E N) : (Vec E (s N))])
ensure the above program works, and introduce implicit arguments for type automatically(that is, no need to write out {A : Type} -> (List A)
, but just (List A)
).
There are many solutions
Or we can define something ridiculous:
(def identity : (-> Nat Nat)
[true => z]
[false => (s z)])
For example, the proof
(def (symm [x y : A] [p : (≡ x y)]) : (≡ y x)
[x y refl => refl])
x
, y
, and p
are explicit, but A
is implicit.
The very basic idea of without-K is that x = x
can't be pattern matched as refl
. The rest of the work of without-K is preventing you from doing the same thing indirectly.
On this, questions are
We should be able to define the following code:
(def (cong {A B : Type}
{x y : A}
[f : (-> A B)]
[P : (≡ x y)])
: (≡ (f x) (f y))
[f refl => refl])
Blocked by #21
The following code shouldn't work but pass our type checking:
(def (foo [x : Nat]) : Bool
[x => x])
This is because we didn't check the function body correctly.
NOTE: Worth taking a look into https://github.com/yjqww6/macrology/blob/master/intdef-ctx.md
(data Zero : Type)
(data One : Type
[one : One])
(data Bool : Type
[true : Bool]
[false : Bool])
(data Nat : Type
[z : Nat]
[s (n : Nat) : Nat])
The current bind is like
(def (foo [x : A] [y : A]) : A
[x => y])
would be good to have
(def (foo [x y : A]) : A
[x => y])
It's easy to find data
's definition is a list of postulate definitions, with such reusing implicit parameters can be done in one place! So I propose the following syntax.
(def f : T
#:postulate)
(def (f [p : P] ...) : T
#:postulate)
And for constructors, syntax will be
(def ...
#:constructor)
Because overlapped binding from racket/base
makes current bounded as constructors is not reliable.
(data Nat : Type
[z : Nat]
[s (n : Nat) : Nat])
to
(def Nat : Type
#:postulate)
(def z : Nat
#:constructor)
(def (s [n : Nat]) : Nat
#:constructor)
(data (≡ {A : Type} [a b : A]) : Type
[refl : (≡ a a)])
to
(def (≡ {A : Type} [a b : A]) : Type
#:postulate)
#|
notice a hard problem here, how to know how many meta came from data type should run into here?
|#
(def (refl {A : Type} {a : A}) : (≡ a a)
#:constructor)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.