Ancestors

Written by Mark Gritter on 2024-12-04 at 19:16

Well, I am stuck and stuck hard on #Ivy. Here's my first toy example: https://gist.github.com/mgritter/17b455a33222e22d2b9627db36c0eaff

I want a system where I provide a left number, then a right number, then update a running sum with the absolute value of their difference.

What I get when I try to state that the sum should be increasing is nonsense models of the numbers like

0:num + 0 = 0

0:num + 1 = 0

1:num + 0 = 0

1:num + 1 = 0

Which is a possible model of the + function, I get it! But I cannot convince Ivy to exclude that model. (I think the model of < may be wrong too, but for some reason it's not including that.)

[#]ModelChecking

@redmp any thoughts on what I'm doing wrong?

=> More informations about this toot | More toots from markgritter@mathstodon.xyz

Toot

Written by Mark Gritter on 2024-12-04 at 22:51

I am wondering if the right thing here is to define an abstract type of "a monotonically increasing sum" first? But it seems like I would run into the same problem.

=> More informations about this toot | More toots from markgritter@mathstodon.xyz

Descendants