Peter Goodall (Nov 20 2021 at 00:25): Peter Goodall (Nov 20 2021 at 00:25):I am tinkering with coding a simple proof by exhaustion. Seems to work ok.
I'd like to display the results clearly. This is part of the code:
println("Associativity")
let
comb = permutationsWithOrder(bools, 3)
for (a, b, c) in comb
@show (a ⊻ b) ⊻ c == a ⊻ (b ⊻ c)
end
end
I get this result, which although comforting to me, I wouldn't ask anyone else to accept it as a proof.
Associativity
(a ⊻ b) ⊻ c == a ⊻ (b ⊻ c) = true
(a ⊻ b) ⊻ c == a ⊻ (b ⊻ c) = true
(a ⊻ b) ⊻ c == a ⊻ (b ⊻ c) = true
...
I need the variables substituted into the expression on the LHS of =. Something like:
(one ⊻ zero) ⊻ zero == one ⊻ (zero ⊻ zero) -> true - I know I’ve done something unorthodox with functions zero and one
I don't want to write a separate expression for display, because it might be less trustworthy. I want to use the exact code of the proof.
I'm wondering if there is an existing macro that does this?
Notification Bot (Nov 20 2021 at 04:52):Peter Goodall has marked this topic as resolved.
Notification Bot (Nov 20 2021 at 04:52):Peter Goodall has marked this topic as unresolved.
Sundar R (Nov 20 2021 at 04:53):So @show shows unevaluated code on the LHS and the evaluation result on the RHS... and you want the same RHS, but LHS to have just the variables evaluated, not the whole expression.
That sounds like an unorthodox requirement, seems unlikely there'd be a standard macro for this already.
Peter Goodall (Nov 20 2021 at 05:07):@Sundar R OK :pray: - makes sense.
I’ll see if anyone else has an idea, otherwise I’ll enjoy another diversion, and learn to write macros. Of-course from where I am, I can't tell if this is feasible yet.
Syx Pek (Nov 20 2021 at 06:20):It might be a good idea to make show allow $() expressions for this purpose
Kwaku Oskin (Nov 20 2021 at 09:04):May be use interpolation?
Instead of @show do something like
println("($a v $b) v $c == $a v ($b v $c) = $((a v b) v c == a v (b v c))"
Sorry, I do not have this logic operator symbol on a phone, so used v instead
Kwaku Oskin (Nov 20 2021 at 09:06):Ah, sorry, missed that you do not want separate expression.
Kwaku Oskin (Nov 20 2021 at 09:07):In that case, yes, some metaprogramming magic is needed. Shouldn't be too hard though, if you have exact and not too big set of rules.
Sukera (Nov 20 2021 at 11:07):Sounds to me like you don't want to eagerly evaluate your formula, but rather construct a lazy representation of it instead, which you can define a show method for that also evaluates, maybe in parts
Sukera (Nov 20 2021 at 11:08):would probably also be more handy to manipulate - though at some point, you may end up with a TSP solver
Sundar R (Nov 20 2021 at 15:41):Syx Pek said:
It might be a good idea to make show allow $() expressions for this purpose
There's a "# TODO: implement interpolated strings" in base/show.jl:1655 next to a function that @show uses, and afaict it's referring to the same idea. So apparently it's on the todo list, just not implemented yet.
Peter Goodall (Nov 20 2021 at 22:56):Andrey Oskin said:
In that case, yes, some metaprogramming magic is needed. Shouldn't be too hard though, if you have exact and not too big set of rules.
It's probably a good first real exercise. I'm guessing a general case would be tricky. I think it will look something like interpolated strings. Two arguments [ list of variables to interpolate, the expression to interpolate then @show ]
Peter Goodall (Nov 20 2021 at 22:58):Sukera said:
would probably also be more handy to manipulate - though at some point, you may end up with a TSP solver
I'm pretty sure I'm not ready to do a general solution - thanks for pointing out where it might lead.
Peter Goodall (Nov 20 2021 at 22:59):I'll have a go, interpolated println() first, then try the macro. Will report back :-)
Sundar R (Nov 20 2021 at 23:16):There's a MacroTools.jl package, in case you weren't aware of it. postwalk might be pretty useful for this.
Sundar R (Nov 20 2021 at 23:20):although, thinking about it, it might not be doable with postwalk :shrug: you might have to copy and modify the show_unquoted function from base/show.jl:1655 that I mentioned above. Not sure about any of this, just giving pointers in case they're helpful.
Sundar R (Nov 20 2021 at 23:21):I made an attempt several hours ago (when you posted this), using postwalk, but I was trying to be too generic and gave up after a while. That's when I ended up at the show_unquoted function.
Peter Goodall (Nov 27 2021 at 01:10):@Andrey Oskin If I'd known enough - I would have followed your suggestion :-)
I spent quite some time learning about macros, MacroTools.jl and Match.jl. I also enjoyed watching "JuliaCon 2020 | Advanced Metaprogramming Tools | Mike Innes".
The result is that I much better understand what I'm asking for, and what the tools do. Maybe Cassette would do what I want. I wrote something pretty simple - which does the job ( abbreviated):
function run_identity(str)
evp = eval ∘ Meta.parse
evp("@show " * str)
end
# pvo=permutationsWithOrder(source-set, tuple-size)
# Associativity by exhaustion - feasible because 𝔹 is a small type.
pr("Associativity")
let
comb = pwo(bools, 3)
for (a, b, c) in comb
run_identity("($a ⊻ $b) ⊻ $c == $a ⊻ ($b ⊻ $c)")
end
end
[...]
Associativity
(one ⊻ zero) ⊻ zero == one ⊻ (zero ⊻ zero) = true
(zero ⊻ one) ⊻ one == zero ⊻ (one ⊻ one) = true
(one ⊻ zero) ⊻ one == one ⊻ (zero ⊻ one) = true
(zero ⊻ zero) ⊻ one == zero ⊻ (zero ⊻ one) = true
(one ⊻ one) ⊻ one == one ⊻ (one ⊻ one) = true
(zero ⊻ zero) ⊻ zero == zero ⊻ (zero ⊻ zero) = true
(zero ⊻ one) ⊻ zero == zero ⊻ (one ⊻ zero) = true
(one ⊻ one) ⊻ zero == one ⊻ (one ⊻ zero) = true
Commutativity
zero ⊻ one == one ⊻ zero = true
one ⊻ zero == zero ⊻ one = true
one ⊻ one == one ⊻ one = true
zero ⊻ zero == zero ⊻ zero = true
Self-inverting
zero ⊻ zero == 𝕫 = true
one ⊻ one == 𝕫 = true
Peter Goodall has marked this topic as resolved.
Last updated: Nov 22 2024 at 04:41 UTC