[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Vic Putz <vbputz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 10:11:02 -0800 (PST)

In https://groups.google.com/u/1/g/tlaplus/c/jnlmYhh4jmo/m/HTGFDZimCAAJ, when asked about a generic hash function in TLA, Ron Pressler wrote:

> Unless what you're specifying is at the level of the hash function itself, you might be

> thinking about this at too-low a level. If the algorithm you're specifying should work with

> any hash function, make that a part of your specification: ∃ hash ∈ [Source → Bits].... If

> there are other requirements on the hash, add them to the quantifier.

Which is a lovely high-level way to specify that such a function exists. I'm facing something similar in a toy spec I'm trying to write for a transpiler, where I can say there exists such a function mapping instructions on architecture A to those on Architecture B, something like ∃ TranslateFn ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B]. Good so far.

I'd like to use that function in a TLC model, but just using the existential quantifier doesn't expose TranslateFn. So the next thing that looks right is TranslateFn == CHOOSE f ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B] : TRUE , because I don't care what that function is, just that there is one and that I can use it.

But won't that ask TLC to (senselessly?) explore the whole space of possible mapping functions? If so, is there a way around that?

Cheers; still learning (slowly...)

-- I'd like to use that function in a TLC model, but just using the existential quantifier doesn't expose TranslateFn. So the next thing that looks right is TranslateFn == CHOOSE f ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B] : TRUE , because I don't care what that function is, just that there is one and that I can use it.

But won't that ask TLC to (senselessly?) explore the whole space of possible mapping functions? If so, is there a way around that?

Cheers; still learning (slowly...)

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/df467f71-77d1-4bed-a83c-d126d5da226fn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Next by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Previous by thread:
**Re: [tlaplus] Utilizing refinement in an inductive proof** - Next by thread:
**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC** - Index(es):