1. Not finding help here? Sign up for a free 30min tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Program Verification - Translation rule

  1. Jan 24, 2012 #1
    Hi

    I am doing a course on Program verification and am having trouble with the properties of summation, more specifically the rule of translation:

    "Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

    [itex]\left\langle[/itex] [itex]\Sigma[/itex]k[itex]\in[/itex]K:R:T[itex]\right\rangle[/itex] = [itex]\left\langle[/itex] [itex]\Sigma[/itex]j[itex]\in[/itex]J:R[k:=f.j]:T[k:=f.j][itex]\right\rangle[/itex]

    My question: I actually do not understand how the LHS of the equation equals the RHS.
    Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?
     
  2. jcsd
  3. Jan 24, 2012 #2

    Mark44

    Staff: Mentor

    Please fix your LaTeX so that it is readable. I can't tell what you're trying to say, so I can't fix it.
     
  4. Jan 25, 2012 #3
    Sorry. Here is my next attempt:

    "Suppose function f maps values of type J to values of type K, and suppose g is a function that maps values of type K to values of type J. suppose further that f and g are inverses. That is, suppose that, for all j[itex]\in[/itex]J and k[itex]\in[/itex]K, (f.j=k) [itex]\equiv[/itex] (j=g.k)

    [itex]\langle[/itex] [itex]\Sigma[/itex]k[itex]\in[/itex]K:R:T[itex]\rangle[/itex] = [itex]\langle[/itex] [itex]\Sigma[/itex]j[itex]\in[/itex]J:R[k:=f.j]:T[k:=f.j][itex]\rangle[/itex]

    My question: I actually do not understand how the LHS of the equation equals the RHS.
    Perhaps more specifically I am not sure how R[k:=f.j] and T[k:=f.j] appears on the right side, where does it come from?
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook




Similar Discussions: Program Verification - Translation rule
  1. Answer verification (Replies: 0)

Loading...