Difficulties with solving the exercises in the K Framework Tutorial

Question

Tutorial 1 Lesson 8 ( mu-defined )

My attempt is to substitute the existing rule : "rule mu X . E => E[(mu X . E) / X]"

with the rule :

    rule mu X:KVar . E:Exp
    => let X =
    (lambda $x . (( lambda X . E) (lambda $y . ($x $x $y))))
    (lambda $x . (( lambda X . E) (lambda $y . ($x $x $y))))    [macro]"

Unfortanetely it wont compile. What am i doing wrong ? Is this solution correct ?

Tutorial 1 Lesson 8 ( SK-combinators )

They have this part in the README of the exercise:

" For example, lambda x . if x then y else z cannot be transformed into combinators as is, but it can if we assume a builtin conditional function constant, say cond, and desugar if_then_else_ to it. Then this expression becomes lambda x . (((cond x) y) z), which we know how to transform. "

My struggle is with ' say cond, and desugar if_then_else_ to it. '

How do i do this part ? Any help would be appreciated.

Tutorial 2 Lesson 4 (purely-syntactic)

They have this part in the README of the exercise:

'Hint: make sequential composition strict(1) or seqstrict, and have statements reduce to {} instead of .; and don't forget to make {} a KResult (you may need a new syntactic category for that, which only includes {} and is included in KResult).'

My struggle is with the part: ' and have statements reduce to {} instead of .; and don't forget to make {} a KResult (you may need a new syntactic category for that, which only includes {} and is included in KResult)'

How do i do this ? Any hints ?

Tutorial 2 Lesson 4 (uninitialized-variables)

I have created the following module:

module UNDEFINED

    rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->"##") </state>
    requires notBool (X in keys(Rho))

endmodule

But this initializes variables with "##". How do i initialize a variable with "undefined" ? Any hints ?

Tutorial 3 Lesson 1 (callCC)

For this exercise i created a very similar code similar to the callcc:

    syntax Exp ::= "callCC" Exp  [strict]
    syntax Val ::= cc(K)
    rule <k> (callCC V:Val => V cc(K)) ~> _ </k>
    rule <k> cc(K) V ~> _ =>  V ~> _ </k>

For some reason it wont compile . What am i doing wrong ? Is this solution correct ?