Greg Exercise 02 - bound names, other grammars

[Jake-Gillberg]

Give the domain equation and the scala (or haskell) representations for the grammars of:

• blue calculus
• ambient process calculus
• (extra credit) linear lambda calculus

Add the definitions free and bound names to the scala (or haskell) representation of rho calculus

[Jake-Gillberg]

https://gist.github.com/Jake-Gillberg/c661903026c0616acebeb8ec93e47db3

[golovach-ivan]

@Jake-Gillberg
I think you variant is not fully correct.

Meredith, Radestock, 2005, "A Reflective Higher-order Calculus":

We now come to one of the first real subtleties of this calculus. Both the
calculation of the free names of a process and the determination of structural congruence between processes critically depend on being able to establish whether two names are equal.

So FN MUST use name equality ≡_N in set operations ('∪' and '\'), not implicitly standard case classes equality (in Scala Set operations ('+', '-', '|', '&~')).

Let P = for(@0 <- @(@0!(0))).((for(@0 <- @(0|0)).0)

FN(P) = {@(@0!(0))} ∪ (FN(for(@0 <- @(0|0)).0) \ {@0}) = {@(@0!(0))} ∪ (FN(@(0|0))) \ {@0}) = {@(@0!(0))} ∪ ( {@(0|0)} \ {@0} ) =
and
= {@(@0!(0))} ∪ ( {@0} \ {@0} ) = {@(@0!(0))} ∪ {} = {@(@0!(0))}
NOT
= {@(@0!(0))} ∪ {@(0|0)} = {@(@0!(0))} ∪ {@(0|0)} = {@(@0!(0)), @(0|0)}

P.S. Because @(0|0) ≡_N @0

[Jake-Gillberg]

@golovach-ivan Ah, yup! You are totally correct, thanks! I have a definition of name equality and structural equality working in scala here, but I don't preserve the structure of bound names, so it would be difficult to implement the Free and Bound name definitions without some modifications.

[golovach-ivan]

@Jake-Gillberg
About Scala code style (IMHO):

1. please, add usage example

2. if method mody is one expression - do not use curve brackets (lines: 31+38, 42+48, 68+73, etc)

// not
    override def equals(other: Any): Boolean = {
      other match {
        case that: Quote => p == that.p
        case _ => false
      }
    }
// but
    override def equals(other: Any): Boolean = other match {
      case that: Quote => p == that.p
      case _ => false
    }

// not
    override val hashCode: Int = {
      41 + p.hashCode
    }
// but
    override val hashCode: Int = 41 + p.hashCode

3. with tuple members you can use assigning to pattern with named vals in for-comprehension (hard to understand this: if input._1._1 == lift._1._1)

  val p = for (
    (name, age, (_, houseNum)) <- Seq(("Mike", 42, ("StreetA", "house#1")), ("Anna", 25, ("StreetA", "house#1")))
  ) yield name

4. place something and compation object for it - together

private final type FreqMap[X] = Map[X, Int]
private final object FreqMap {
  def empty[X] = Map.empty[X, Int]
}

5. class without body does not need empty curve brackets

// not
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1),
                                               height = 0 ) {
  }
// but
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1),
                                               height = 0 ) 

6. use type params inference

// not
  final object Zero extends Process(
    inputs = FreqMap.empty[(Name, Process)],
    lifts = FreqMap.empty[(Name, Process)],
    drops = FreqMap.empty[Name],
    height = 0)
// but
  final object Zero extends Process(
    inputs = FreqMap.empty,
    lifts = FreqMap.empty,
    drops = FreqMap.empty,
    height = 0)

7. Move constructors default values from children to parent (maybe?)

  sealed class Process(val inputs: Inputs = FreqMap.empty,
                                   val lifts: Lifts = FreqMap.empty,
                                   val drops: Drops = FreqMap.empty,
                                   val height: Int = 0)

  final object Zero extends Process

  final class Drop(x: Name) extends Process(drops = Map(x -> 1))

  final class Parallel(p: Process, q: Process) extends Process(
    inputs = mergeMaps(Seq(p.inputs, q.inputs)),
    lifts = mergeMaps(Seq(p.lifts, q.lifts)),
    drops = mergeMaps(Seq(p.drops, q.drops)),
    height = math.max(p.height, q.height))

  final class Lift(x: Name, p: Process) extends Process(
    lifts = Map((x, p) -> 1),
    height = p.height)

  final class Input(y: Name, x: Name, p: Process) extends Process(
    inputs = Map((x, substitute(y, BoundName(p.height), p)) -> 1),
    height = p.height + 1)

8. from math point of view (in my opinion) you do not need '41 +' here

// not
    override val hashCode: Int = {
      41 + p.hashCode
    }
// but
    override val hashCode: Int = p.hashCode

9. it can be more consistent to use FreqMap constructor not Map

// not
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1), // <<<=== HERE
                                               height = 0 ) {
  }
// but
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = FreqMap(x -> 1),
                                               height = 0 ) {
  }
  private final object FreqMap {
    ...
    def apply[X, B](elems: (X, Int)*): FreqMap[X] = Map[X, Int](elems: _*)
  }

10. personally i like

// this
object FreqMap {
  def apply[X] = Map.empty[X, Int]
}
val x: FreqMap[String] = FreqMap()
val y: Seq[Int] = Seq()

// not this
object FreqMap {
  def empty[X] = Map.empty[X, Int]
}
val x: FreqMap[String] = FreqMap.empty()
val y: Seq[Int] = Seq.empty()

[kayvank]

@Jake-Gillberg I finally caught up with Greg's lectures & am trying to catch up with the HW now. Here is my take on the 1st HW, FreeName computations.
https://github.com/kayvank/calculi

[kayvank]

@Jake-Gillberg Here my take on the Arabic-numerals assignment:
https://github.com/kayvank/arabic-numerals

[kayvank]

A few category theory resources:

• Bartosz Milesski, https://bartoszmilewski.com/, here is a link to his book: https://github.com/hmemcpy/milewski-ctfp-pdf

• Mike Stay presentation: https://www.youtube.com/watch?v=rZawYtTdObo