dannypsnl / k Goto Github PK

View Code? Open in Web Editor NEW

11.0 4.0 1.0 287 KB

k theorem prover

Home Page: https://pkgs.racket-lang.org/package/k

License: Apache License 2.0

Racket 98.76% Julia 1.24%

racket theorem-prover

k's Introduction

k

Warning This is a developing project

K is a theorem prover based on Racket ecosystem, interact with Racket in useful way is the major purpose of the project.

Installation

only want core language
```
raco pkg install --auto k-core
```

wants standard library

raco pkg install --auto k-core
raco pkg install --auto k-lib

Usage

NOTE: implicit parameter haven't implemented, the following is a bit pseudo code

(def (symm {A : Type} {x y : A}
           [P : (≡ x y)])
  : (≡ y x)
  [refl => refl])

(def (trans {A : Type}
            {x y z : A}
            [P1 : (≡ x y)]
            [P2 : (≡ y z)])
  : (≡ x z)
  [refl refl => refl])

For developer

The following commands might be helpful for your development

raco pkg install --auto ./k-core
raco pkg install --auto ./k-lib
raco pkg install --auto ./k-doc
raco pkg install --auto ./k-test
raco pkg install --auto ./k-example
# apply git config of the project
git config commit.template $(pwd)/.gitmessage

k's People

Contributors

Stargazers

Watchers

Forkers

cybai

k's Issues

def identity

Currently, the following code cannot work

(def (identity [a : A]) : A
  [a => a])

improve pattern transformation

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.

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.

references

https://github.com/RedPRL/mugenjou

nested pattern won't work currently

#36 constructs an example for it.

Example: Fibonacci

(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.

doc initial

Need more description for our forms and libraries:

data
def
check
typeof
libraries:
- k/data/nat
- k/data/bool
- k/data/list
- k/data/vec
- k/equality

postulate definition for later reuse it in `data`

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.

Example

Nat

(data Nat : Type
      [z : Nat]
      [s (n : Nat) : Nat])

(def Nat : Type
  #:postulate)
(def z : Nat
  #:constructor)
(def (s [n : Nat]) : Nat
  #:constructor)

equality

(data (≡ {A : Type} [a b : A]) : Type
      [refl : (≡ a a)])

(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)

redundant `begin`

https://github.com/racket-tw/k/blob/develop/k-core/k/core.rkt#L35-L42

equivalence type

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.

syntax: data-out

For now, we have to write

(provide Nat s z)

We want

(provide (data-out Nat))

NOTE: https://docs.racket-lang.org/reference/stxtrans.html#%28def._%28%28lib._racket%2Fprovide-transform..rkt%29._make-provide-transformer%29%29

def should check its patterns' type

Or we can define something ridiculous:

(def identity : (-> Nat Nat)
  [true => z]
  [false => (s z)])

BUG: def with one clause will be treated as variable binding, which is a problem

For example:

(def identity : (-> A A)
  [m => m])

bind many name with type

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])

extract bindings
update data type bindings
update data type constructor bindings
update def bindings

unknown reason crashed on pkgs.racket-lang.org

https://pkg-build.racket-lang.org/server/built/archive-fail/k.txt

The interesting part is our CI do not crash

path

Cubical/HoTT variant language, e.g. #lang k/ube

left, right
idp?

Proof examples

(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)))])

Bad type should work without strict positivity

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

try merge `#:postulate` and `#:constructor`

The only difference is their syntax-property so I think they are mergeable.

Observational equality

funext
funext2

finite set

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

data type with dependencies(PI type): like Vec, List

(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)).

add failed test

To ensure our type checker works well with ill-form, we need a test set for cases that shall fail.

implement pi type correctly

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.

turn to multi-collection project

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

support basic data type syntax: Zero, One, Bool, Nat

(data Zero : Type)
(data One : Type
  [one : One])
(data Bool : Type
  [true : Bool]
  [false : Bool])
(data Nat : Type
  [z : Nat]
  [s (n : Nat) : Nat])

Abbreviation for `Pi`

(define-syntax-parser →
  [(_ A B) #'(Pi ([_ : A]) B)])

I guess also rename it out as ->

Quantitative type theory

Infinity is readonly
1 can be compiled to an inplace modification
0 can be only used in type

without-K

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

Should we implement cubical/homotopy based on this?
How to do it correctly?

covering check

We have to ensure a definition is covering(no paths get ignored).

depends on term's type cannot work

#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`

strictly positive check

(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

test is not working

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?

simpler index type

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)])])

implicit parameter and implicit pattern

Racket

https://docs.racket-lang.org/syntax-classes/index.html#%28form._%28%28lib._syntax%2Fparse%2Fclass%2Fparen-shape..rkt%29._~7ebraces%29%29

The link is how to match brace

usage

And this is required for ≡ type:

(data (≡ {A : Type} [a b : A]) : Type
      [refl : (≡ a a)])

Syntax

(≡ A b c) ; good, apply implicit
(≡ b c) ; good
; same in pattern, full is all implicit

Fix implicit definition's expansion

(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.

Generated syntax's(from datum) identifier became free identifier even it has bound originally

(check (≡ (* (s z) (s z))
          (s (s (s (s (s z))))))
       (refl))

normalize term in type properly

(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.

check body of def function

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

Real

reference:

https://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf

termination check

There are many solutions

structural recursion
sized type(mini-agda, but inconsistent)

bug(`Nat=?` cannot type check now)

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)])