freenode/#sicl - IRC Chatlog
Search
12:42:12
Bike
"CONS types. Only (CONS T T) and variants, as well as (CONS NIL *), etc are strictly supported." well that's a worrying comment
12:43:59
Bike
since it's baker, it tries to give every type a bit vector (or actually a number, but it's treated as a bit vector)
12:44:51
Bike
for a cons type it does that recursively with the car and cdr. if they're both -1 (T) it returns the bit vector for cons. if either is 0 (NIL) it returns 0. otherwise it gives up, which seems to result in subtypep returning NIL NIL
12:48:04
beach
I think Baker's method works for everything except (CONS <t1> <t2>) in the general case.
12:52:46
beach
So it looks to me like Baker's algorithm splits each "leaf type (or set)" into elementary sets that do not overlap, and then the problem becomes equivalent to determining whether a set composed of the union, intersection, and complement of these elementary sets is necessarily the empty set.
12:55:04
beach
And this formula ought to be possible to express as something that can be solved by an SMT solver.
12:56:11
Bike
you can do 3-sat with satisfies types, if subtypep lets them be subtypes of themselves
13:01:13
beach
Now, (CONS <t1> <t2) is a subtype of (CONS <t3> <t4>) if and only if <t1> is a subtype of <t3> and <t2> is a subtype of <t4>, right?
13:02:09
beach
So apparently Baker's method fails to express that as a bunch of elementary non-overlapping sets.
13:02:40
MichaelRaskin
Although that might not be true for some very optimised and case-by-case cons implementations (that also don't seem too reasonable for Lisp)
13:04:05
MichaelRaskin
In principle one could have cons-of-(unsigned-byte 8)-or-null as a special optimised representation that is only used when the type is declared and this special representation is not a subtype of cons-of-number-or-null
13:06:46
MichaelRaskin
Hm. Maybe it is indeed better to have types as values (to be able to provide an axiom for CONS with a quantifier over types)
13:09:11
MichaelRaskin
One can either try to expand CONS before asking FO or SMT solver, or provide an axiom to the solver to deal with CONS.
13:12:01
beach
Hmm, wait! Could one use a recursive invocation of SUBTYPEP to split those occurrences of CONS types into elementary non-overlapping sets?
13:17:08
beach
I should also re-read Jim's dissertation to see whether his algorithm for splitting sets into non-overlapping subsets handles CONS types.
13:20:56
MichaelRaskin
Hopefully yes, but probably without caring about exponential growth (because every part of the algorithm already has this exponential growth)
13:22:53
MichaelRaskin
Of course, we don't know what practical purposes will arise once there is a library with subtypep that works well
13:23:58
beach
Now, in the case where there is exponential growth, would an axiom-based technique behave badly as well?
13:24:26
MichaelRaskin
Depends. Everything from SAT-solvers and up has quite a bit of black magic inside.
13:26:34
MichaelRaskin
In the most general case you can probably model worst-case SAT problem, whatever is the worst case for the chosen tool. And many people believe in SETH, i.e. the worst case for every SAT-solver is exponential.
17:11:21
fiddlerwoaroof
hi, I've been trying to use SICL recently and I've run into a couple issues.
17:12:22
fiddlerwoaroof
1) the README says to start a repl with (repl ee4) which uses an undefined symbol EE4 and calls an undefined function REPL
17:13:31
fiddlerwoaroof
2) When I load sicl-boot-inspector, I get a couple errors: first, I get INSPECT is not external in package CLOUSEAU
17:14:14
fiddlerwoaroof
3) If I fix that (export 'clouseau::inspect (find-package :clouseau)), I get this error: https://github.com/robert-strandh/SICL/issues/145#issuecomment-544271263
18:14:56
beach
fiddlerwoaroof: I haven't re-implemented the REPL after major changes to the boot procedure.
20:04:57
fiddlerwoaroof
Shinmera: I know, I just remembered a while ago it was possible to get a repl and run some simple code and I was looking to see how things are progressing
20:07:14
fiddlerwoaroof
beach: interesting, I had double-checked my installation of mcclim, but I think git was looking in the wrong place for some reason
21:24:23
Bike
beach has been doing a lot of work on sicl and booting specifically, so those instructions arne't really valid any more