[Agda] Strict application

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

If you want to formalize call-by-value lambda-calculus (instead of
cbn, which you do below), you would need some concept of value.

For your concrete example below, the only values are lambdas, so you
could try

  beta : forall f g -> app (lam f) (lam g) \equiv f (lam g).

But usually cbv lambda-calculus includes variables in the concept of
values, so that you can also reason about open terms.

Cheers,
Andreas

On 26.04.2014 18:00, Andrés Sicard-Ramírez wrote:
> 
> On 26 April 2014 10:28, Wolfram Kahl <kahl at cas.mcmaster.ca 
> <mailto:kahl at cas.mcmaster.ca>> wrote:
> 
>> {-# NO_TERMINATION_CHECK #-} loop : ℕ loop = loop
>> 
>> foo : ℕ foo = (λ _ → 0) loop
> 
> This is not Agda code (or, if you want, is is ``illegal Agda
> code''): You are only allowed to use {-# NO_TERMINATION_CHECK #-} 
> where you have a separate termination proof.
> 
> 
> I agree. That is ``illegal Agda code''.
> 
> Let _≡_ be the propositional equality. I can formalise a
> non-strict application (beta) by
> 
> postulate D    : Set app  : D → D → D lam  : (D → D) → D beta : ∀ f
> a → app (lam f) a ≡ f a
> 
> Using the same approach, can I formalise a strict application?
> 
> Best,
> 
> -- Andrés
> 
> 
> _______________________________________________ Agda mailing list 
> Agda at lists.chalmers.se 
> https://lists.chalmers.se/mailman/listinfo/agda
> 


- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlNcxcgACgkQPMHaDxpUpLPdiQCggY2tIq3Wa3C0qNBfSDfEY3L6
xHkAnj4eCEm1V97RuH06tkPCic82TPvJ
=LyE2
-----END PGP SIGNATURE-----