| 6 Oct 2021 |
 apache8080 | Where does the IELE group discuss things? Looks like their matrix is dead | 16:15:39 |
 everett.hildenbrandt | Here should be fine actually. | 16:29:07 |
| everett.hildenbrandt | If you have questions about the language itself and the semantics. | 16:29:20 |
| apache8080 | Does IELE get used by any production blockchains? | 16:43:21 |
|  javbit joined the room. | 16:44:48 |
| everett.hildenbrandt | Not at the moment. | 17:19:18 |
| 9 Oct 2021 |
|  @ammkrn:matrix.org left the room. | 21:02:36 |
| 14 Oct 2021 |
|  Sashmit Bhaduri joined the room. | 21:11:09 |
| 15 Oct 2021 |
|  jesse.sigal joined the room. | 20:41:59 |
| 19 Oct 2021 |
|  koding joined the room. | 06:35:08 |
| koding | Hi all! Is Jello Paper website being updated?
(I had difficulties to get beyond Installation as it is the only item after Homepage in the left-hand menu. It took me a while to understand that the content of Repository Structure section is the main content of the Jello Paper -- only thanks to the Web Archive versions of the website from 2019.) | 06:49:01 |
| everett.hildenbrandt | Yes, it is updated automatically whenever KEVM is updated (https://github.com/kframework/evm-semantics). The left navigation menu gives you high-level navigation, and the right one gives you low-level navigation. | 16:25:34 |
| 20 Oct 2021 |
| jesse.sigal | Hi all, is it possible to have alpha equivalnce taken into account when using kprove? I.e., in my language I want claim (\x -> x) => (\y -> y) to work (where x and y are program variables). | 14:25:07 |
| jesse.sigal | (and (\x -> x) is lambda syntax) | 14:29:37 |
| 21 Oct 2021 |
| everett.hildenbrandt | Not like this (without writing your own manual pattern matching), because from K's perspective these are just terms that look like \->(x, x) and \->(y, y) where \-> is the symbol defined in your language. | 12:29:50 |
| jesse.sigal | Is there a common idiom in K for acheiving this? (Based on or not with KVars) | 12:30:33 |
| everett.hildenbrandt | But if you put symbolic variables in for x and y then at least this case will work:
claim (\X:Var -> X) => (\?Y:Var -> ?Y)
for example. | 12:30:36 |
| everett.hildenbrandt | But from K's perspective in your original, x and y are "domain values" (which means they are distinct elements in the carrier sort in the model). | 12:31:40 |
| everett.hildenbrandt | Whereas X:Var is a symbolic universally quantified variable, and ?Y:Var is an existentially quantified variable. | 12:32:09 |
| everett.hildenbrandt | But weird things happen at the 0-step proof boundary, so i fyou want to do a functional equality proof like this, you may want to force it to take one step, I usually do this:
syntax Step ::= run ( MySort ) , done ( MySort )
rule k run(X) => done(X) ... /k
claim k run(\X:Var -> X) => done(\?Y:Var -> Y) ... /k
to force it to do a single step of execution before checking the equality. | 12:33:44 |
| jesse.sigal | Ah I believe I ran into this issue yesterday experimenting where it complained no rewrites were applicable :) | 12:34:42 |
| jesse.sigal | Thanks! | 12:35:22 |
| jesse.sigal | I guess it's also possible to write a K function to replace all bound (w.r.t. the defined language) variables with existential/fresh K variables as a preparation step. | 12:36:23 |
| everett.hildenbrandt | Yes, it's definitely possible, but it's maybe not as straightforward as you may think. | 12:38:12 |
| everett.hildenbrandt | You can have a rule that looks like this:
rule k makeFresh() => ?X:Int ... /k
for example. | 12:38:31 |
| everett.hildenbrandt | But you can't have a functional rule like that, because the semantics of having a fresh existential variable on the RHS of a functional rule ends up being unsound. | 12:39:00 |
| everett.hildenbrandt | So you need to manually unfold your whole term on the top of the k cell, and replace variables using top-level semantic rules like above, and then re-fold it back up. | 12:39:36 |
| jesse.sigal | Hmmm, makes sense that that would cause problems. I'll have to sit and think about the last point you made as well.
As a plus, the calculus I implemented as a test has a reduction relation which is functional, so I might be able to get away with a simpler approach. | 12:41:43 |
| everett.hildenbrandt | eg. (sketch):
rule k (\X:Var -> TERM) => #applySubst(X, ?XFRESH, TERM) ~> (\?XFRESH -> [HOLE]) ... /k
rule k TERM ~> (\X -> [HOLE]) => (\X -> TERM) ... /k
syntax MySort ::= #applySubst(Var, Var, MySort) [function]
rule #applySubst(X, ?XFRESH, X) => ?XFRESH
... OTHER CASES FORE #applySubst | 12:42:24 |
| jesse.sigal | Ah I think I see, cheers! | 12:47:40 |
