Skip to main content
Theoretical Computer Science

Return to Question

Corrected a little mistake in one example
Source Link
Alejandro DC
Alejandro DC
  • 701
  • 3
  • 14

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is it possible to construct a function $f$ taking two terms and returning a type such that $f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

  • $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R\to T}.t)~s}>=T$$f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R}.t^T)~s}>=T$

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is it possible to construct a function $f$ taking two terms and returning a type such that $f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

  • $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R\to T}.t)~s}>=T$

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is it possible to construct a function $f$ taking two terms and returning a type such that $f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

  • $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R}.t^T)~s}>=T$

Change of notation; edited body
Source Link
Alejandro DC
Alejandro DC
  • 701
  • 3
  • 14

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is isit possible to construct a function $f$ taking two terms and returning a type such that $f^{\Lambda X.t}_{r}$$f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f_{\lambda x^T.x}^{\Lambda X.\lambda x^{X\to X}.t}=T$$f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

  • $f_{(\lambda x^{R\to T}.t)~s}^{\Lambda X.\lambda x^X.r}=T$$f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R\to T}.t)~s}>=T$

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is is possible to construct a function $f$ taking two terms and returning a type such that $f^{\Lambda X.t}_{r}$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f_{\lambda x^T.x}^{\Lambda X.\lambda x^{X\to X}.t}=T$.

  • $f_{(\lambda x^{R\to T}.t)~s}^{\Lambda X.\lambda x^X.r}=T$

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is it possible to construct a function $f$ taking two terms and returning a type such that $f<{\Lambda X.t}><{r}>$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

  • $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R\to T}.t)~s}>=T$

Source Link
Alejandro DC
Alejandro DC
  • 701
  • 3
  • 14

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is is possible to construct a function $f$ taking two terms and returning a type such that $f^{\Lambda X.t}_{r}$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

  • $f_{\lambda x^T.x}^{\Lambda X.\lambda x^{X\to X}.t}=T$.

  • $f_{(\lambda x^{R\to T}.t)~s}^{\Lambda X.\lambda x^X.r}=T$