alim
  • Member for 5 years, 6 months
  • Last seen more than 1 year ago
1 answers
3 votes
187 views
how type checking fails?
Accepted answer
2 votes

I finally figured it out. The key is using sub-typing rules. ctx[]|- t:S ctx[]|S<:T ---------------------------t-sub ctx[]|-t:T By applying this rule after T-...

View answer
2 answers
5 votes
1k views
what is variable capture in nominal logic?
1 votes

I find out it. in the higher-order unification, some function is found for variable $X$ such as $ [X \mapsto \lambda y.y ]$, substituting this for $X$ will not lead to variable capture. in nominal ...

View answer
1 answers
3 votes
59 views
What algorithm solves high-order unification for untyped terms in most cases?
1 votes

Maybe you should try nominal unification. In the paper nominal unification, it gives 4 examples which are untyped $\lambda$-terms.

View answer
1 answers
0 votes
53 views
occur-check, does nominal unification has it?
Accepted answer
1 votes

Yes, it has the occur check. The ~variable transformation rule of nominal unification has a condition which states provided X does not occur in t what it is saying is exactly occur check.

View answer
2 answers
3 votes
61 views
how to use type application rule (T-TAPP)?
Accepted answer
0 votes

I figured it out. there is a unification needed during type checking. there is a condition though, $ftv(T_2) \in \Gamma_{tv}$, saying free type variables of $T2$ should be found in the set of type ...

View answer
4 answers
5 votes
200 views
How to use Type application Rule to get a desired type
0 votes

T11 is can be find on derivation on the right branch of that rule for type checking. On the right hand branch, you will eventually have {x:T}|-x:T11 something like this. You apply "T_VAR" rule ...

View answer
3 answers
3 votes
85 views
A question about type rule
Accepted answer
-1 votes

"T1" is obtained from typing context by doing derivation on the right branch of application rule. I worked on some type checking examples and concluded that.

View answer